Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem lmbr 7866

Description: Express the binary relation "sequence converges to point " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition allows us to use objects more general than sequences when convenient; see the comment in df-lm 7860.

Hypothesis

Ref	Expression
lmbr.1

Assertion

Ref	Expression
lmbr	Met

Distinct variable groups:   ,,,   ,,,   ,,,

---

Proof of Theorem lmbr

Step	Hyp	Ref	Expression
1		simpll 412	. . 3 Met Met
2		brrelex 3197	. . . . . 6
3		lmrel 7865	. . . . . 6 Met
4	2, 3	sylan 448	. . . . 5 Met
5	4	anim1i 334	. . . 4 Met
6	5	an1rs 488	. . 3 Met
7	1, 6	jca 288	. 2 Met Met
8		pm3.26 319	. . . . 5 Met Met
9		ssexg 2711	. . . . . . . . 9
10		dmexg 3344	. . . . . . . . . . . 12 Met
11		dmexg 3344	. . . . . . . . . . . 12
12	10, 11	syl 10	. . . . . . . . . . 11 Met
13		lmbr.1	. . . . . . . . . . 11
14	12, 13	syl5eqel 1544	. . . . . . . . . 10 Met
15		axcnex 5239	. . . . . . . . . . 11
16		xpexg 3249	. . . . . . . . . . 11
17	15, 16	mpan 693	. . . . . . . . . 10
18	14, 17	syl 10	. . . . . . . . 9 Met
19	9, 18	sylan2 451	. . . . . . . 8 Met
20	19	ancoms 436	. . . . . . 7 Met
21	20	adantrl 394	. . . . . 6 Met
22		simprl 414	. . . . . 6 Met
23	21, 22	jca 288	. . . . 5 Met
24	8, 23	jca 288	. . . 4 Met Met
25	24	anassrs 441	. . 3 Met Met
26	25	3ad2antr1 810	. 2 Met Met
27	13	lmfval 7863	. . . 4 Met
28		breq 2611	. . . 4
29	27, 28	syl 10	. . 3 Met
30		sseq1 2072	. . . . 5
31		fveq1 3708	. . . . . . . . . . 11
32	31	eleq1d 1532	. . . . . . . . . 10
33	31	opreq1d 3960	. . . . . . . . . . 11
34	33	breq1d 2619	. . . . . . . . . 10
35	32, 34	anbi12d 626	. . . . . . . . 9
36	35	imbi2d 610	. . . . . . . 8
37	36	rexralbidv 1674	. . . . . . 7
38	37	imbi2d 610	. . . . . 6
39	38	ralbidv 1655	. . . . 5
40	30, 39	3anbi13d 892	. . . 4
41		eleq1 1526	. . . . 5
42		opreq2 3954	. . . . . . . . . . 11
43	42	breq1d 2619	. . . . . . . . . 10
44	43	anbi2d 614	. . . . . . . . 9
45	44	imbi2d 610	. . . . . . . 8
46	45	rexralbidv 1674	. . . . . . 7
47	46	imbi2d 610	. . . . . 6
48	47	ralbidv 1655	. . . . 5