Theorem metelcls 7916

Description: A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. Warning: The HTML proof page is 0.5MB in size.

Hypotheses

Ref	Expression
metelcls.1	|- X = dom dom D
metelcls.2	|- J = (Open` D)
metelcls.3	|- P e. V

Assertion

Ref	Expression
metelcls	|- ((D e. Met /\ M (_ X) -> (P e. ((cls` J)` M) <-> E.f(f:NN-->M /\ f(~~>m` D)P)))

Distinct variable groups:   D,f   f,J   f,M   P,f   f,X

Proof of Theorem metelcls

Step	Hyp	Ref	Expression
1		nnex 5889	. . . . . . . 8 |- NN e. V
2		snex 2745	. . . . . . . 8 |- {P} e. V
3	1, 2	xpex 3255	. . . . . . 7 |- (NN X. {P}) e. V
4		feq1 3612	. . . . . . . 8 |- (f = (NN X. {P}) -> (f:NN-->M <-> (NN X. {P}):NN-->M))
5		breq1 2617	. . . . . . . 8 |- (f = (NN X. {P}) -> (f(~~>m` D)P <-> (NN X. {P})(~~>m` D)P))
6	4, 5	anbi12d 627	. . . . . . 7 |- (f = (NN X. {P}) -> ((f:NN-->M /\ f(~~>m` D)P) <-> ((NN X. {P}):NN-->M /\ (NN X. {P})(~~>m` D)P)))
7	3, 6	cla4ev 1865	. . . . . 6 |- (((NN X. {P}):NN-->M /\ (NN X. {P})(~~>m` D)P) -> E.f(f:NN-->M /\ f(~~>m` D)P))
8		snssi 2462	. . . . . . . 8 |- (P e. M -> {P} (_ M)
9		metelcls.3	. . . . . . . . . 10 |- P e. V
10	9	fconst 3649	. . . . . . . . 9 |- (NN X. {P}):NN-->{P}
11		fss 3626	. . . . . . . . 9 |- (((NN X. {P}):NN-->{P} /\ {P} (_ M) -> (NN X. {P}):NN-->M)
12	10, 11	mpan 694	. . . . . . . 8 |- ({P} (_ M -> (NN X. {P}):NN-->M)
13	8, 12	syl 10	. . . . . . 7 |- (P e. M -> (NN X. {P}):NN-->M)
14	13	adantl 388	. . . . . 6 |- (((D e. Met /\ M (_ X) /\ P e. M) -> (NN X. {P}):NN-->M)
15		metelcls.1	. . . . . . . . 9 |- X = dom dom D
16		1z 6114	. . . . . . . . 9 |- 1 e. ZZ
17		nnuz 6379	. . . . . . . . 9 |- NN = (ZZ>` 1)
18	15, 16, 17	lmconst 7886	. . . . . . . 8 |- ((D e. Met /\ P e. X) -> (NN X. {P})(~~>m` D)P)
19		ssel2 2060	. . . . . . . 8 |- ((M (_ X /\ P e. M) -> P e. X)
20	18, 19	sylan2 451	. . . . . . 7 |- ((D e. Met /\ (M (_ X /\ P e. M)) -> (NN X. {P})(~~>m` D)P)
21	20	anassrs 441	. . . . . 6 |- (((D e. Met /\ M (_ X) /\ P e. M) -> (NN X. {P})(~~>m` D)P)
22	7, 14, 21	sylanc 471	. . . . 5 |- (((D e. Met /\ M (_ X) /\ P e. M) -> E.f(f:NN-->M /\ f(~~>m` D)P))
23	22	adantlr 393	. . . 4 |- ((((D e. Met /\ M (_ X) /\ P e. ((cls` J)` M)) /\ P e. M) -> E.f(f:NN-->M /\ f(~~>m` D)P))
24		eqid 1473	. . . . . . . 8 |- U.J = U.J
25	24	islpi 7699	. . . . . . 7 |- (((J e. Top /\ M (_ U.J) /\ (P e. ((cls` J)` M) /\ -. P e. M)) -> P e. ((limPt` J)` M))
26		metelcls.2	. . . . . . . . . 10 |- J = (Open` D)
27	26	opntop 7822	. . . . . . . . 9 |- (D e. Met -> J e. Top)
28	27	adantr 389	. . . . . . . 8 |- ((D e. Met /\ M (_ X) -> J e. Top)
29	15, 26	uniopn 7813	. . . . . . . . . 10 |- (D e. Met -> U.J = X)
30	29	sseq2d 2085	. . . . . . . . 9 |- (D e. Met -> (M (_ U.J <-> M (_ X))
31	30	biimpar 417	. . . . . . . 8 |- ((D e. Met /\ M (_ X) -> M (_ U.J)
32	28, 31	jca 288	. . . . . . 7 |- ((D e. Met /\ M (_ X) -> (J e. Top /\ M (_ U.J))
33	25, 32	sylan 448	. . . . . 6 |- (((D e. Met /\ M (_ X) /\ (P e. ((cls` J)` M) /\ -. P e. M)) -> P e. ((limPt` J)` M))
34	15, 26	lpbl 7832	. . . . . . . . . . 11 |- (((D e. Met /\ M (_ X /\ P e. ((limPt` J)` M)) /\ ((1 / j) e. RR /\ 0 < (1 / j))) -> E.y e. M y e. (P( ball ` D)(1 / j)))
35		nnrecret 6223	. . . . . . . . . . . 12 |- (j e. NN -> (1 / j) e. RR)
36		nnrecgt0t 5908	. . . . . . . . . . . 12 |- (j e. NN -> 0 < (1 / j))
37	35, 36	jca 288	. . . . . . . . . . 11 |- (j e. NN -> ((1 / j) e. RR /\ 0 < (1 / j)))
38	34, 37	sylan2 451	. . . . . . . . . 10 |- (((D e. Met /\ M (_ X /\ P e. ((limPt` J)` M)) /\ j e. NN) -> E.y e. M y e. (P( ball ` D)(1 / j)))
39	38	r19.21aiva 1711	. . . . . . . . 9 |- ((D e. Met /\ M (_ X /\ P e. ((limPt` J)` M)) -> A.j e. NN E.y e. M y e. (P( ball ` D)(1 / j)))
40	39	3expa 832	. . . . . . . 8 |- (((D e. Met /\ M (_ X) /\ P e. ((limPt` J)` M)) -> A.j e. NN E.y e. M y e. (P( ball ` D)(1 / j)))
41		eleq1 1531	. . . . . . . . 9 |- (y = (f` j) -> (y e. (P( ball ` D)(1 / j)) <-> (f` j) e. (P( ball ` D)(1 / j))))
42	1, 41	ac6s 4736	. . . . . . . 8 |- (A.j e. NN E.y e. M y e. (P( ball ` D)(1 / j)) -> E.f(f:NN-->M /\ A.j e. NN (f` j) e. (P( ball ` D)(1 / j))))
43	40, 42	syl 10	. . . . . . 7 |- (((D e. Met /\ M (_ X) /\ P e. ((limPt` J)` M)) -> E.f(f:NN-->M /\ A.j e. NN (f` j) e. (P( ball ` D)(1 / j))))
44		ssel2 2060	. . . . . . . . 9 |- ((((limPt` J)` M) (_ X /\ P e. ((limPt` J)` M)) -> P e. X)
45	24	lpss 7696	. . . . . . . . . . 11 |- ((J e. Top /\ M (_ U.J) -> ((limPt` J)` M) (_ U.J)
46	45, 28, 31	sylanc 471	. . . . . . . . . 10 |- ((D e. Met /\ M (_ X) -> ((limPt` J)` M) (_ U.J)
47	29	adantr 389	. . . . . . . . . 10 |- ((D e. Met /\ M (_ X) -> U.J = X)
48	46, 47	sseqtrd 2093	. . . . . . . . 9 |- ((D e. Met /\ M (_ X) -> ((limPt` J)` M) (_ X)
49	44, 48	sylan 448	. . . . . . . 8 |- (((D e. Met /\ M (_ X) /\ P e. ((limPt` J)` M)) -> P e. X)
50		simprl 414	. . . . . . . . . . 11 |- ((((D e. Met /\ M (_ X) /\ P e. X) /\ (f:NN-->M /\ A.j e. NN (f` j) e. (P( ball ` D)(1 / j)))) -> f:NN-->M)
51		fss 3626	. . . . . . . . . . . . . . . . . . 19 |- ((f:NN-->M /\ M (_ X) -> f:NN-->X)
52	51	ex 373	. . . . . . . . . . . . . . . . . 18 |- (f:NN-->M -> (M (_ X -> f:NN-->X))
53	52	com12 11	. . . . . . . . . . . . . . . . 17 |- (M (_ X -> (f:NN-->M -> f:NN-->X))
54	53	adantl 388	. . . . . . . . . . . . . . . 16 |- ((D e. Met /\ M (_ X) -> (f:NN-->M -> f:NN-->X))
55	54	adantr 389	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ M (_ X) /\ P e. X) -> (f:NN-->M -> f:NN-->X))
56	55	anim1d 559	. . . . . . . . . . . . . 14 |- (((D e. Met /\ M (_ X) /\ P e. X) -> ((f:NN-->M /\ A.j e. NN (f` j) e. (P( ball ` D)(1 / j))) -> (f:NN-->X /\ A.j e. NN (f` j) e. (P( ball ` D)(1 / j)))))
57	15	elbl3 7792	. . . . . . . . . . . . . . . . . 18 |- (((D e. Met /\ P e. X /\ (f` j) e. X) /\ ((1 / j) e. RR /\ 0 < (1 / j))) -> ((f` j) e. (P( ball ` D)(1 / j)) <-> ((f` j)DP) < (1 / j)))
58		id 59	. . . . . . . . . . . . . . . . . . . . 21 |- ((D e. Met /\ P e. X /\ (f` j) e. X) -> (D e. Met /\ P e. X /\ (f` j) e. X))
59	58	3expa 832	. . . . . . . . . . . . . . . . . . . 20 |- (((D e. Met /\ P e. X) /\ (f` j) e. X) -> (D e. Met /\ P e. X /\ (f` j) e. X))
60		ffvelrn 3805	. . . . . . . . . . . . . . . . . . . 20 |- ((f:NN-->X /\ j e. NN) -> (f` j) e. X)
61	59, 60	sylan2 451	. . . . . . . . . . . . . . . . . . 19 |- (((D e. Met /\ P e. X) /\ (f:NN-->X /\ j e. NN)) -> (D e. Met /\ P e. X /\ (f` j) e. X))
62	61	anassrs 441	. . . . . . . . . . . . . . . . . 18 |- ((((D e. Met /\ P e. X) /\ f:NN-->X) /\ j e. NN) -> (D e. Met /\ P e. X /\ (f` j) e. X))
63	37	adantl 388	. . . . . . . . . . . . . . . . . 18 |- ((((D e. Met /\ P e. X) /\ f:NN-->X) /\ j e. NN) -> ((1 / j) e. RR /\ 0 < (1 / j)))
64	57, 62, 63	sylanc 471	. . . . . . . . . . . . . . . . 17 |- ((((D e. Met /\ P e. X) /\ f:NN-->X) /\ j e. NN) -> ((f` j) e. (P( ball ` D)(1 / j)) <-> ((f` j)DP) < (1 / j)))
65	64	ralbidva 1656	. . . . . . . . . . . . . . . 16 |- ((