# 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 ) =/= (/) ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`