Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem lmfval 7863

Description: The relation "sequence converges to point " in a metric space.

Hypothesis

Ref	Expression
lmfval.1

Assertion

Ref	Expression
lmfval	Met

Distinct variable groups:   ,,,,,   ,,

---

Proof of Theorem lmfval

Step	Hyp	Ref	Expression
1		xpexg 3249	. . . 4
2		dmexg 3344	. . . . . . 7 Met
3		dmexg 3344	. . . . . . 7
4	2, 3	syl 10	. . . . . 6 Met
5		lmfval.1	. . . . . 6
6	4, 5	syl5eqel 1544	. . . . 5 Met
7		axcnex 5239	. . . . . 6
8		xpexg 3249	. . . . . 6
9	7, 8	mpan 693	. . . . 5
10		pwexg 2736	. . . . 5
11	6, 9, 10	3syl 20	. . . 4 Met
12	1, 11, 6	sylanc 471	. . 3 Met
13		df-3an 775	. . . . . . 7
14		visset 1804	. . . . . . . . 9
15	14	elpw 2394	. . . . . . . 8
16	15	3anbi1i 822	. . . . . . 7
17	13, 16	bitr3 175	. . . . . 6
18	17	opabbii 2661	. . . . 5
19		opabssxp 3224	. . . . 5
20	18, 19	eqsstr3 2082	. . . 4
21		ssexg 2711	. . . 4
22	20, 21	mpan 693	. . 3
23	12, 22	syl 10	. 2 Met
24		dmeq 3300	. . . . . . . . 9
25	24	dmeqd 3302	. . . . . . . 8
26	25, 5	syl6eqr 1517	. . . . . . 7
27		xpeq2 3191	. . . . . . 7
28	26, 27	syl 10	. . . . . 6
29	28	sseq2d 2079	. . . . 5
30	26	eleq2d 1533	. . . . 5
31	26	eleq2d 1533	. . . . . . . . . 10
32	31	anbi1d 615	. . . . . . . . 9
33	32	imbi2d 610	. . . . . . . 8
34	33	rexralbidv 1674	. . . . . . 7
35	34	imbi2d 610	. . . . . 6
36	35	ralbidv 1655	. . . . 5
37	29, 30, 36	3anbi123d 890	. . . 4
38	37	opabbidv 2660	. . 3