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 ffvelrnda 
 |-  ( ( ( ( ( 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 43 rexeqdv 
 |-  ( ( ( ( ( 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 ) <-> E. x e. S x e. ( g ` n ) ) )
45 35 44 mpbird 
 |-  ( ( ( ( ( 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 ) )
46 45 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 ) )
47 fvex 
 |-  ( _I ` S ) e. _V
48 nnenom 
 |-  NN ~~ _om
49 eleq1 
 |-  ( x = ( f ` n ) -> ( x e. ( g ` n ) <-> ( f ` n ) e. ( g ` n ) ) )
50 47 48 49 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 ) ) )
51 46 50 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 ) ) )
52 42 feq3d 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> ( f : NN --> ( _I ` S ) <-> f : NN --> S ) )
53 52 biimpd 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> ( f : NN --> ( _I ` S ) -> f : NN --> S ) )
54 53 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 ) )
55 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 )
56 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 ) )
57 eleq2 
 |-  ( x = y -> ( P e. x <-> P e. y ) )
58 fveq2 
 |-  ( k = j -> ( g ` k ) = ( g ` j ) )
59 58 sseq1d 
 |-  ( k = j -> ( ( g ` k ) C_ x <-> ( g ` j ) C_ x ) )
60 59 cbvrexvw 
 |-  ( E. k e. NN ( g ` k ) C_ x <-> E. j e. NN ( g ` j ) C_ x )
61 sseq2 
 |-  ( x = y -> ( ( g ` j ) C_ x <-> ( g ` j ) C_ y ) )
62 61 rexbidv 
 |-  ( x = y -> ( E. j e. NN ( g ` j ) C_ x <-> E. j e. NN ( g ` j ) C_ y ) )
63 60 62 syl5bb 
 |-  ( x = y -> ( E. k e. NN ( g ` k ) C_ x <-> E. j e. NN ( g ` j ) C_ y ) )
64 57 63 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 ) ) )
65 64 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 ) )
66 56 65 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 ) )
67 simpr 
 |-  ( ( P e. ( g ` k ) /\ ( g ` ( k + 1 ) ) C_ ( g ` k ) ) -> ( g ` ( k + 1 ) ) C_ ( g ` k ) )
68 67 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 ) )
69 9 68 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 ) )
70 69 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 ) )
71 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 )
72 fveq2 
 |-  ( n = j -> ( g ` n ) = ( g ` j ) )
73 72 sseq1d 
 |-  ( n = j -> ( ( g ` n ) C_ ( g ` j ) <-> ( g ` j ) C_ ( g ` j ) ) )
74 73 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 ) ) ) )
75 fveq2 
 |-  ( n = m -> ( g ` n ) = ( g ` m ) )
76 75 sseq1d 
 |-  ( n = m -> ( ( g ` n ) C_ ( g ` j ) <-> ( g ` m ) C_ ( g ` j ) ) )
77 76 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 ) ) ) )
78 fveq2 
 |-  ( n = ( m + 1 ) -> ( g ` n ) = ( g ` ( m + 1 ) ) )
79 78 sseq1d 
 |-  ( n = ( m + 1 ) -> ( ( g ` n ) C_ ( g ` j ) <-> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) )
80 79 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 ) ) ) )
81 ssid 
 |-  ( g ` j ) C_ ( g ` j )
82 81 2a1i 
 |-  ( j e. ZZ -> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` j ) C_ ( g ` j ) ) )
83 eluznn 
 |-  ( ( j e. NN /\ m e. ( ZZ>= ` j ) ) -> m e. NN )
84 fvoveq1 
 |-  ( k = m -> ( g ` ( k + 1 ) ) = ( g ` ( m + 1 ) ) )
85 fveq2 
 |-  ( k = m -> ( g ` k ) = ( g ` m ) )
86 84 85 sseq12d 
 |-  ( k = m -> ( ( g ` ( k + 1 ) ) C_ ( g ` k ) <-> ( g ` ( m + 1 ) ) C_ ( g ` m ) ) )
87 86 rspccva 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ m e. NN ) -> ( g ` ( m + 1 ) ) C_ ( g ` m ) )
88 83 87 sylan2 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ ( j e. NN /\ m e. ( ZZ>= ` j ) ) ) -> ( g ` ( m + 1 ) ) C_ ( g ` m ) )
89 88 anassrs 
 |-  ( ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) /\ m e. ( ZZ>= ` j ) ) -> ( g ` ( m + 1 ) ) C_ ( g ` m ) )
90 sstr2 
 |-  ( ( g ` ( m + 1 ) ) C_ ( g ` m ) -> ( ( g ` m ) C_ ( g ` j ) -> ( g ` ( m + 1 ) ) C_ ( g ` j ) ) )
91 89 90 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 ) ) )
92 91 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 ) ) ) )
93 92 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 ) ) ) )
94 74 77 80 77 82 93 uzind4 
 |-  ( m e. ( ZZ>= ` j ) -> ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( g ` m ) C_ ( g ` j ) ) )
95 94 com12 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> ( m e. ( ZZ>= ` j ) -> ( g ` m ) C_ ( g ` j ) ) )
96 95 ralrimiv 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) C_ ( g ` k ) /\ j e. NN ) -> A. m e. ( ZZ>= ` j ) ( g ` m ) C_ ( g ` j ) )
97 70 71 96 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 ) )
98 fveq2 
 |-  ( n = m -> ( f ` n ) = ( f ` m ) )
99 98 75 eleq12d 
 |-  ( n = m -> ( ( f ` n ) e. ( g ` n ) <-> ( f ` m ) e. ( g ` m ) ) )
100 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 ) )
101 100 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 ) )
102 71 83 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 )
103 99 101 102 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 ) )
104 103 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 ) )
105 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 ) ) )
106 97 104 105 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 ) ) )
107 ssel2 
 |-  ( ( ( g ` m ) C_ ( g ` j ) /\ ( f ` m ) e. ( g ` m ) ) -> ( f ` m ) e. ( g ` j ) )
108 107 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 ) )
109 106 108 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 ) )
110 ssel 
 |-  ( ( g ` j ) C_ y -> ( ( f ` m ) e. ( g ` j ) -> ( f ` m ) e. y ) )
111 110 ralimdv 
 |-  ( ( g ` j ) C_ y -> ( A. m e. ( ZZ>= ` j ) ( f ` m ) e. ( g ` j ) -> A. m e. ( ZZ>= ` j ) ( f ` m ) e. y ) )
112 109 111 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 ) )
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 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 ) )
115 114 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 ) )
116 66 115 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 ) )
117 116 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 ) )
118 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 )
119 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
120 118 119 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 ) )
121 nnuz 
 |-  NN = ( ZZ>= ` 1 )
122 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 )
123 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 )
124 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 )
125 123 124 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 )
126 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 ) )
127 120 121 122 125 126 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 ) ) ) )
128 55 117 127 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 )
129 128 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 ) )
130 129 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 ) ) )
131 54 130 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 ) ) )
132 131 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 ) ) )
133 51 132 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 ) )
134 8 133 exlimddv 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ P e. ( ( cls ` J ) ` S ) ) -> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) )
135 134 ex 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) -> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )
136 3 ad2antrr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> J e. Top )
137 136 119 sylib 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> J e. ( TopOn ` X ) )
138 1zzd 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> 1 e. ZZ )
139 simprr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> f ( ~~>t ` J ) P )
140 simprl 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> f : NN --> S )
141 140 ffvelrnda 
 |-  ( ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) /\ k e. NN ) -> ( f ` k ) e. S )
142 simplr 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> S C_ X )
143 121 137 138 139 141 142 lmcls 
 |-  ( ( ( J e. 1stc /\ S C_ X ) /\ ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) -> P e. ( ( cls ` J ) ` S ) )
144 143 ex 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( ( f : NN --> S /\ f ( ~~>t ` J ) P ) -> P e. ( ( cls ` J ) ` S ) ) )
145 144 exlimdv 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) -> P e. ( ( cls ` J ) ` S ) ) )
146 135 145 impbid 
 |-  ( ( J e. 1stc /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )