Metamath Proof Explorer

Theorem 1stcelcls

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. This proof uses countable choice ax-cc . A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis 1stcelcls.1 
|- X = U. J
Assertion 1stcelcls 
|- ( ( J e. 1stc /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )

Proof

Step Hyp Ref Expression
1 1stcelcls.1 
 |-  X = U. J
2 simpll 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> J e. 1stc )
3 1stctop 
 |-  ( J e. 1stc -> J e. Top )
4 1 clsss3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
5 3 4 sylan 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
6 5 sselda 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> P e. X )
7 1 1stcfb 
 |-  ( ( J e. 1stc /\ P e. X ) -> E. g ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) )
8 2 6 7 syl2anc 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> E. g ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) )
9 simpr2 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) )
10 simpl 
 |-  ( ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) -> P e. ( g ` k ) )
11 10 ralimi 
 |-  ( A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) -> A. k e. NN P e. ( g ` k ) )
12 9 11 syl 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> A. k e. NN P e. ( g ` k ) )
13 fveq2 
 |-  ( k = n -> ( g ` k ) = ( g ` n ) )
14 13 eleq2d 
 |-  ( k = n -> ( P e. ( g ` k ) <-> P e. ( g ` n ) ) )
15 14 rspccva 
 |-  ( ( A. k e. NN P e. ( g ` k ) /\ n e. NN ) -> P e. ( g ` n ) )
16 12 15 sylan 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> P e. ( g ` n ) )
17 eleq2 
 |-  ( y = ( g ` n ) -> ( P e. y <-> P e. ( g ` n ) ) )
18 ineq1 
 |-  ( y = ( g ` n ) -> ( y i^i S ) = ( ( g ` n ) i^i S ) )
19 18 neeq1d 
 |-  ( y = ( g ` n ) -> ( ( y i^i S ) =/= (/) <-> ( ( g ` n ) i^i S ) =/= (/) ) )
20 17 19 imbi12d 
 |-  ( y = ( g ` n ) -> ( ( P e. y -> ( y i^i S ) =/= (/) ) <-> ( P e. ( g ` n ) -> ( ( g ` n ) i^i S ) =/= (/) ) ) )
21 1 elcls2 
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) ) )
22 3 21 sylan 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) ) ) )
23 22 simplbda 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) )
24 23 ad2antrr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> A. y e. J ( P e. y -> ( y i^i S ) =/= (/) ) )
25 simpr1 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> g : NN --> J )
26 25 ffvelcdmda 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> ( g ` n ) e. J )
27 20 24 26 rspcdva 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> ( P e. ( g ` n ) -> ( ( g ` n ) i^i S ) =/= (/) ) )
28 16 27 mpd 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> ( ( g ` n ) i^i S ) =/= (/) )
29 elin 
 |-  ( x e. ( ( g ` n ) i^i S ) <-> ( x e. ( g ` n ) /\ x e. S ) )
30 29 biancomi 
 |-  ( x e. ( ( g ` n ) i^i S ) <-> ( x e. S /\ x e. ( g ` n ) ) )
31 30 exbii 
 |-  ( E. x x e. ( ( g ` n ) i^i S ) <-> E. x ( x e. S /\ x e. ( g ` n ) ) )
32 n0 
 |-  ( ( ( g ` n ) i^i S ) =/= (/) <-> E. x x e. ( ( g ` n ) i^i S ) )
33 df-rex 
 |-  ( E. x e. S x e. ( g ` n ) <-> E. x ( x e. S /\ x e. ( g ` n ) ) )
34 31 32 33 3bitr4i 
 |-  ( ( ( g ` n ) i^i S ) =/= (/) <-> E. x e. S x e. ( g ` n ) )
35 28 34 sylib 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> E. x e. S x e. ( g ` n ) )
36 3 ad2antrr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> J e. Top )
37 1 topopn 
 |-  ( J e. Top -> X e. J )
38 36 37 syl 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> X e. J )
39 simplr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> S C_ X )
40 38 39 ssexd 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> S e. _V )
41 fvi 
 |-  ( S e. _V -> ( _I ` S ) = S )
42 40 41 syl 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> ( _I ` S ) = S )
43 42 ad2antrr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> ( _I ` S ) = S )
44 35 43 rexeqtrrdv 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ n e. NN ) -> E. x e. ( _I ` S ) x e. ( g ` n ) )
45 44 ralrimiva 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> A. n e. NN E. x e. ( _I ` S ) x e. ( g ` n ) )
46 fvex 
 |-  ( _I ` S ) e. _V
47 nnenom 
 |-  NN ~~ _om
48 eleq1 
 |-  ( x = ( f ` n ) -> ( x e. ( g ` n ) <-> ( f ` n ) e. ( g ` n ) ) )
49 46 47 48 axcc4 
 |-  ( A. n e. NN E. x e. ( _I ` S ) x e. ( g ` n ) -> E. f ( f : NN --> ( _I ` S ) /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) )
50 45 49 syl 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> E. f ( f : NN --> ( _I ` S ) /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) )
51 42 feq3d 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> ( f : NN --> ( _I ` S ) <-> f : NN --> S ) )
52 51 biimpd 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> ( f : NN --> ( _I ` S ) -> f : NN --> S ) )
53 52 adantr 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> ( f : NN --> ( _I ` S ) -> f : NN --> S ) )
54 6 ad2antrr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> P e. X )
55 simplr3 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) )
56 eleq2 
 |-  ( x = y -> ( P e. x <-> P e. y ) )
57 fveq2 
 |-  ( k = j -> ( g ` k ) = ( g ` j ) )
58 57 sseq1d 
 |-  ( k = j -> ( ( g ` k ) C_ x <-> ( g ` j ) C_ x ) )
59 58 cbvrexvw 
 |-  ( E. k e. NN ( g ` k ) C_ x <-> E. j e. NN ( g ` j ) C_ x )
60 sseq2 
 |-  ( x = y -> ( ( g ` j ) C_ x <-> ( g ` j ) C_ y ) )
61 60 rexbidv 
 |-  ( x = y -> ( E. j e. NN ( g ` j ) C_ x <-> E. j e. NN ( g ` j ) C_ y ) )
62 59 61 bitrid 
 |-  ( x = y -> ( E. k e. NN ( g ` k ) C_ x <-> E. j e. NN ( g ` j ) C_ y ) )
63 56 62 imbi12d 
 |-  ( x = y -> ( ( P e. x -> E. k e. NN ( g ` k ) C_ x ) <-> ( P e. y -> E. j e. NN ( g ` j ) C_ y ) ) )
64 63 rspccva 
 |-  ( ( A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) /\ y e. J ) -> ( P e. y -> E. j e. NN ( g ` j ) C_ y ) )
65 55 64 sylan 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) /\ y e. J ) -> ( P e. y -> E. j e. NN ( g ` j ) C_ y ) )
66 simpr 
 |-  ( ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) -> ( g ` ( k + 1 ) ) C_ ( g ` k ) )
67 66 ralimi 
 |-  ( A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) -> A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) )
68 9 67 syl 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) )
69 68 adantr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) )
70 simprrr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> j e. NN )
71 fveq2 
 |-  ( n = j -> ( g ` n ) = ( g ` j ) )
72 71 sseq1d 
 |-  ( n = j -> ( ( g ` n ) C_ ( g ` j ) <-> ( g ` j ) C_ ( g ` j ) ) )
73 72 imbi2d 
 |-  ( n = j -> ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` n ) C_ ( g ` j ) ) <-> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` j ) C_ ( g ` j ) ) ) )
74 fveq2 
 |-  ( n = m -> ( g ` n ) = ( g ` m ) )
75 74 sseq1d 
 |-  ( n = m -> ( ( g ` n ) C_ ( g ` j ) <-> ( g ` m ) C_ ( g ` j ) ) )
76 75 imbi2d 
 |-  ( n = m -> ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` n ) C_ ( g ` j ) ) <-> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` m ) C_ ( g ` j ) ) ) )
77 fveq2 
 |-  ( n = ( m + 1 ) -> ( g ` n ) = ( g ` ( m + 1 ) ) )
78 77 sseq1d 
 |-  ( n = ( m + 1 ) -> ( ( g ` n ) C_ ( g ` j ) <-> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) )
79 78 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` n ) C_ ( g ` j ) ) <-> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) ) )
80 ssid 
 |-  ( g ` j ) C_ ( g ` j )
81 80 2a1i 
 |-  ( j e. ZZ -> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` j ) C_ ( g ` j ) ) )
82 eluznn 
 |-  ( ( j e. NN /\ m e. ( ZZ>= ` j ) ) -> m e. NN )
83 fvoveq1 
 |-  ( k = m -> ( g ` ( k + 1 ) ) = ( g ` ( m + 1 ) ) )
84 fveq2 
 |-  ( k = m -> ( g ` k ) = ( g ` m ) )
85 83 84 sseq12d 
 |-  ( k = m -> ( ( g ` ( k + 1 ) ) C_ ( g ` k ) <-> ( g ` ( m + 1 ) ) C_ ( g ` m ) ) )
86 85 rspccva 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ m e. NN ) -> ( g ` ( m + 1 ) ) C_ ( g ` m ) )
87 82 86 sylan2 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ ( j e. NN /\ m e. ( ZZ>= ` j ) ) ) -> ( g ` ( m + 1 ) ) C_ ( g ` m ) )
88 87 anassrs 
 |-  ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) /\ m e. ( ZZ>= ` j ) ) -> ( g ` ( m + 1 ) ) C_ ( g ` m ) )
89 sstr2 
 |-  ( ( g ` ( m + 1 ) ) C_ ( g ` m ) -> ( ( g ` m ) C_ ( g ` j ) -> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) )
90 88 89 syl 
 |-  ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) /\ m e. ( ZZ>= ` j ) ) -> ( ( g ` m ) C_ ( g ` j ) -> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) )
91 90 expcom 
 |-  ( m e. ( ZZ>= ` j ) -> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( ( g ` m ) C_ ( g ` j ) -> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) ) )
92 91 a2d 
 |-  ( m e. ( ZZ>= ` j ) -> ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` m ) C_ ( g ` j ) ) -> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) ) )
93 73 76 79 76 81 92 uzind4 
 |-  ( m e. ( ZZ>= ` j ) -> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` m ) C_ ( g ` j ) ) )
94 93 com12 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( m e. ( ZZ>= ` j ) -> ( g ` m ) C_ ( g ` j ) ) )
95 94 ralrimiv 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> A. m e. ( ZZ>= ` j ) ( g ` m ) C_ ( g ` j ) )
96 69 70 95 syl2anc 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> A. m e. ( ZZ>= ` j ) ( g ` m ) C_ ( g ` j ) )
97 fveq2 
 |-  ( n = m -> ( f ` n ) = ( f ` m ) )
98 97 74 eleq12d 
 |-  ( n = m -> ( ( f ` n ) e. ( g ` n ) <-> ( f ` m ) e. ( g ` m ) ) )
99 simplr 
 |-  ( ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) -> A. n e. NN ( f ` n ) e. ( g ` n ) )
100 99 ad2antlr 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) /\ m e. ( ZZ>= ` j ) ) -> A. n e. NN ( f ` n ) e. ( g ` n ) )
101 70 82 sylan 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. NN )
102 98 100 101 rspcdva 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) /\ m e. ( ZZ>= ` j ) ) -> ( f ` m ) e. ( g ` m ) )
103 102 ralrimiva 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. ( g ` m ) )
104 r19.26 
 |-  ( A. m e. ( ZZ>= ` j ) ( ( g ` m ) C_ ( g ` j ) /\ ( f ` m ) e. ( g ` m ) ) <-> ( A. m e. ( ZZ>= ` j ) ( g ` m ) C_ ( g ` j ) /\ A. m e. ( ZZ>= ` j ) ( f ` m ) e. ( g ` m ) ) )
105 96 103 104 sylanbrc 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> A. m e. ( ZZ>= ` j ) ( ( g ` m ) C_ ( g ` j ) /\ ( f ` m ) e. ( g ` m ) ) )
106 ssel2 
 |-  ( ( ( g ` m ) C_ ( g ` j ) /\ ( f ` m ) e. ( g ` m ) ) -> ( f ` m ) e. ( g ` j ) )
107 106 ralimi 
 |-  ( A. m e. ( ZZ>= ` j ) ( ( g ` m ) C_ ( g ` j ) /\ ( f ` m ) e. ( g ` m ) ) -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. ( g ` j ) )
108 105 107 syl 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. ( g ` j ) )
109 ssel 
 |-  ( ( g ` j ) C_ y -> ( ( f ` m ) e. ( g ` j ) -> ( f ` m ) e. y ) )
110 109 ralimdv 
 |-  ( ( g ` j ) C_ y -> ( A. m e. ( ZZ>= ` j ) ( f ` m ) e. ( g ` j ) -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
111 108 110 syl5com 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) /\ ( y e. J /\ j e. NN ) ) ) -> ( ( g ` j ) C_ y -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
112 111 anassrs 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) /\ ( y e. J /\ j e. NN ) ) -> ( ( g ` j ) C_ y -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
113 112 anassrs 
 |-  ( ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) /\ y e. J ) /\ j e. NN ) -> ( ( g ` j ) C_ y -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
114 113 reximdva 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) /\ y e. J ) -> ( E. j e. NN ( g ` j ) C_ y -> E. j e. NN A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
115 65 114 syld 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) /\ y e. J ) -> ( P e. y -> E. j e. NN A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
116 115 ralrimiva 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> A. y e. J ( P e. y -> E. j e. NN A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
117 36 ad2antrr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> J e. Top )
118 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
119 117 118 sylib 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> J e. ( TopOn ` X ) )
120 nnuz 
 |-  NN = ( ZZ>= ` 1 )
121 1zzd 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> 1 e. ZZ )
122 simprl 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> f : NN --> S )
123 39 ad2antrr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> S C_ X )
124 122 123 fssd 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> f : NN --> X )
125 eqidd 
 |-  ( ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) /\ m e. NN ) -> ( f ` m ) = ( f ` m ) )
126 119 120 121 124 125 lmbrf 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> ( f ( ~~>t ` J ) P <-> ( P e. X /\ A. y e. J ( P e. y -> E. j e. NN A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) ) ) )
127 54 116 126 mpbir2and 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) ) -> f ( ~~>t ` J ) P )
128 127 expr 
 |-  ( ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) /\ f : NN --> S ) -> ( A. n e. NN ( f ` n ) e. ( g ` n ) -> f ( ~~>t ` J ) P ) )
129 128 imdistanda 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> ( ( f : NN --> S /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) -> ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )
130 53 129 syland 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> ( ( f : NN --> ( _I ` S ) /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) -> ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )
131 130 eximdv 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> ( E. f ( f : NN --> ( _I ` S ) /\ A. n e. NN ( f ` n ) e. ( g ` n ) ) -> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )
132 50 131 mpd 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g : NN --> J /\ A. k e. NN ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) /\ A. x e. J ( P e. x -> E. k e. NN ( g ` k ) C_ x ) ) ) -> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) )
133 8 132 exlimddv 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) )
134 133 ex 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) -> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )
135 3 ad2antrr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> J e. Top )
136 135 118 sylib 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> J e. ( TopOn ` X ) )
137 1zzd 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> 1 e. ZZ )
138 simprr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> f ( ~~>t ` J ) P )
139 simprl 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> f : NN --> S )
140 139 ffvelcdmda 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) /\ k e. NN ) -> ( f ` k ) e. S )
141 simplr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> S C_ X )
142 120 136 137 138 140 141 lmcls 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> P e. ( ( cls ` J ) ` S ) )
143 142 ex 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( ( f : NN --> S /\ f ( ~~>t ` J ) P ) -> P e. ( ( cls ` J ) ` S ) ) )
144 143 exlimdv 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) -> P e. ( ( cls ` J ) ` S ) ) )
145 134 144 impbid 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )