MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1stcelcls Unicode version

Theorem 1stcelcls 17181
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 8056. 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.)
Hypothesis
Ref Expression
1stcelcls.1  |-  X  = 
U. J
Assertion
Ref Expression
1stcelcls  |-  ( ( J  e.  1stc  /\  S  C_  X )  ->  ( P  e.  ( ( cls `  J ) `  S )  <->  E. f
( f : NN --> S  /\  f ( ~~> t `  J ) P ) ) )
Distinct variable groups:    f, J    P, f    S, f    f, X

Proof of Theorem 1stcelcls
StepHypRef Expression
1 simpll 733 . . . . 5  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  J  e.  1stc )
2 1stctop 17163 . . . . . . 7  |-  ( J  e.  1stc  ->  J  e. 
Top )
3 1stcelcls.1 . . . . . . . 8  |-  X  = 
U. J
43clsss3 16790 . . . . . . 7  |-  ( ( J  e.  Top  /\  S  C_  X )  -> 
( ( cls `  J
) `  S )  C_  X )
52, 4sylan 459 . . . . . 6  |-  ( ( J  e.  1stc  /\  S  C_  X )  ->  (
( cls `  J
) `  S )  C_  X )
65sselda 3181 . . . . 5  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  P  e.  X )
731stcfb 17165 . . . . 5  |-  ( ( 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
) ) )
81, 6, 7syl2anc 645 . . . 4  |-  ( ( ( 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 simpr1 966 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
10 ffvelrn 5624 . . . . . . . . . . . . 13  |-  ( ( g : NN --> J  /\  n  e.  NN )  ->  ( g `  n
)  e.  J )
119, 10sylan 459 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )
123elcls2 16805 . . . . . . . . . . . . . . 15  |-  ( ( 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
)  =/=  (/) ) ) ) )
132, 12sylan 459 . . . . . . . . . . . . . 14  |-  ( ( 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 )  =/=  (/) ) ) ) )
1413simplbda 610 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  A. y  e.  J  ( P  e.  y  ->  ( y  i^i  S )  =/=  (/) ) )
1514ad2antrr 709 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )  =/=  (/) ) )
16 simpr2 967 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) )
17 simpl 445 . . . . . . . . . . . . . . 15  |-  ( ( P  e.  ( g `
 k )  /\  ( g `  (
k  +  1 ) )  C_  ( g `  k ) )  ->  P  e.  ( g `  k ) )
1817ralimi 2619 . . . . . . . . . . . . . 14  |-  ( A. k  e.  NN  ( P  e.  ( g `  k )  /\  (
g `  ( k  +  1 ) ) 
C_  ( g `  k ) )  ->  A. k  e.  NN  P  e.  ( g `  k ) )
1916, 18syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
20 fveq2 5485 . . . . . . . . . . . . . . 15  |-  ( k  =  n  ->  (
g `  k )  =  ( g `  n ) )
2120eleq2d 2351 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  ( P  e.  ( g `  k )  <->  P  e.  ( g `  n
) ) )
2221rspccva 2884 . . . . . . . . . . . . 13  |-  ( ( A. k  e.  NN  P  e.  ( g `  k )  /\  n  e.  NN )  ->  P  e.  ( g `  n
) )
2319, 22sylan 459 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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
) )
24 eleq2 2345 . . . . . . . . . . . . . 14  |-  ( y  =  ( g `  n )  ->  ( P  e.  y  <->  P  e.  ( g `  n
) ) )
25 ineq1 3364 . . . . . . . . . . . . . . 15  |-  ( y  =  ( g `  n )  ->  (
y  i^i  S )  =  ( ( g `
 n )  i^i 
S ) )
2625neeq1d 2460 . . . . . . . . . . . . . 14  |-  ( y  =  ( g `  n )  ->  (
( y  i^i  S
)  =/=  (/)  <->  ( (
g `  n )  i^i  S )  =/=  (/) ) )
2724, 26imbi12d 313 . . . . . . . . . . . . 13  |-  ( y  =  ( g `  n )  ->  (
( P  e.  y  ->  ( y  i^i 
S )  =/=  (/) )  <->  ( P  e.  ( g `  n
)  ->  ( (
g `  n )  i^i  S )  =/=  (/) ) ) )
2827rspcv 2881 . . . . . . . . . . . 12  |-  ( ( g `  n )  e.  J  ->  ( A. y  e.  J  ( P  e.  y  ->  ( y  i^i  S
)  =/=  (/) )  -> 
( P  e.  ( g `  n )  ->  ( ( g `
 n )  i^i 
S )  =/=  (/) ) ) )
2911, 15, 23, 28syl3c 59 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )  =/=  (/) )
30 elin 3359 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( g `
 n )  i^i 
S )  <->  ( x  e.  ( g `  n
)  /\  x  e.  S ) )
31 ancom 439 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( g `
 n )  /\  x  e.  S )  <->  ( x  e.  S  /\  x  e.  ( g `  n ) ) )
3230, 31bitri 242 . . . . . . . . . . . . 13  |-  ( x  e.  ( ( g `
 n )  i^i 
S )  <->  ( x  e.  S  /\  x  e.  ( g `  n
) ) )
3332exbii 1574 . . . . . . . . . . . 12  |-  ( E. x  x  e.  ( ( g `  n
)  i^i  S )  <->  E. x ( x  e.  S  /\  x  e.  ( g `  n
) ) )
34 n0 3465 . . . . . . . . . . . 12  |-  ( ( ( g `  n
)  i^i  S )  =/=  (/)  <->  E. x  x  e.  ( ( g `  n )  i^i  S
) )
35 df-rex 2550 . . . . . . . . . . . 12  |-  ( E. x  e.  S  x  e.  ( g `  n )  <->  E. x
( x  e.  S  /\  x  e.  (
g `  n )
) )
3633, 34, 353bitr4i 270 . . . . . . . . . . 11  |-  ( ( ( g `  n
)  i^i  S )  =/=  (/)  <->  E. x  e.  S  x  e.  ( g `  n ) )
3729, 36sylib 190 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) )
38 simplr 734 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  S  C_  X
)
392ad2antrr 709 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  J  e.  Top )
403topopn 16646 . . . . . . . . . . . . . . 15  |-  ( J  e.  Top  ->  X  e.  J )
4139, 40syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  X  e.  J )
42 ssexg 4161 . . . . . . . . . . . . . 14  |-  ( ( S  C_  X  /\  X  e.  J )  ->  S  e.  _V )
4338, 41, 42syl2anc 645 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  S  e.  _V )
44 fvi 5540 . . . . . . . . . . . . 13  |-  ( S  e.  _V  ->  (  _I  `  S )  =  S )
4543, 44syl 17 . . . . . . . . . . . 12  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  (  _I  `  S )  =  S )
4645ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
4746rexeqdv 2744 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) ) )
4837, 47mpbird 225 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) )
4948ralrimiva 2627 . . . . . . . 8  |-  ( ( ( ( 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 ) )
50 fvex 5499 . . . . . . . . 9  |-  (  _I 
`  S )  e. 
_V
51 nnenom 11036 . . . . . . . . 9  |-  NN  ~~  om
52 eleq1 2344 . . . . . . . . 9  |-  ( x  =  ( f `  n )  ->  (
x  e.  ( g `
 n )  <->  ( f `  n )  e.  ( g `  n ) ) )
5350, 51, 52axcc4 8060 . . . . . . . 8  |-  ( 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
) ) )
5449, 53syl 17 . . . . . . 7  |-  ( ( ( ( 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 ) ) )
55 feq3 5342 . . . . . . . . . . . 12  |-  ( (  _I  `  S )  =  S  ->  (
f : NN --> (  _I 
`  S )  <->  f : NN
--> S ) )
5645, 55syl 17 . . . . . . . . . . 11  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  ( f : NN --> (  _I  `  S )  <->  f : NN
--> S ) )
5756biimpd 200 . . . . . . . . . 10  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  ( f : NN --> (  _I  `  S )  ->  f : NN --> S ) )
5857adantr 453 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
596ad2antrr 709 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )
60 simplr3 1004 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 )
)
61 eleq2 2345 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  ( P  e.  x  <->  P  e.  y ) )
62 fveq2 5485 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
g `  k )  =  ( g `  j ) )
6362sseq1d 3206 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  j  ->  (
( g `  k
)  C_  x  <->  ( g `  j )  C_  x
) )
6463cbvrexv 2766 . . . . . . . . . . . . . . . . . 18  |-  ( E. k  e.  NN  (
g `  k )  C_  x  <->  E. j  e.  NN  ( g `  j
)  C_  x )
65 sseq2 3201 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( g `  j
)  C_  x  <->  ( g `  j )  C_  y
) )
6665rexbidv 2565 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( E. j  e.  NN  ( g `  j
)  C_  x  <->  E. j  e.  NN  ( g `  j )  C_  y
) )
6764, 66syl5bb 250 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  ( E. k  e.  NN  ( g `  k
)  C_  x  <->  E. j  e.  NN  ( g `  j )  C_  y
) )
6861, 67imbi12d 313 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( P  e.  x  ->  E. k  e.  NN  ( g `  k
)  C_  x )  <->  ( P  e.  y  ->  E. j  e.  NN  ( g `  j
)  C_  y )
) )
6968rspccva 2884 . . . . . . . . . . . . . . 15  |-  ( ( 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
) )
7060, 69sylan 459 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 )
)
71 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( P  e.  ( g `
 k )  /\  ( g `  (
k  +  1 ) )  C_  ( g `  k ) )  -> 
( g `  (
k  +  1 ) )  C_  ( g `  k ) )
7271ralimi 2619 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. k  e.  NN  ( P  e.  ( g `  k )  /\  (
g `  ( k  +  1 ) ) 
C_  ( g `  k ) )  ->  A. k  e.  NN  ( g `  (
k  +  1 ) )  C_  ( g `  k ) )
7316, 72syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 )
)
7473adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 ) )
75 simprrr 744 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 )
76 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  j  ->  (
g `  n )  =  ( g `  j ) )
7776sseq1d 3206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  j  ->  (
( g `  n
)  C_  ( g `  j )  <->  ( g `  j )  C_  (
g `  j )
) )
7877imbi2d 309 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) ) ) )
79 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
g `  n )  =  ( g `  m ) )
8079sseq1d 3206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  m  ->  (
( g `  n
)  C_  ( g `  j )  <->  ( g `  m )  C_  (
g `  j )
) )
8180imbi2d 309 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) ) ) )
82 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  ( m  + 
1 )  ->  (
g `  n )  =  ( g `  ( m  +  1
) ) )
8382sseq1d 3206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  ( m  + 
1 )  ->  (
( g `  n
)  C_  ( g `  j )  <->  ( g `  ( m  +  1 ) )  C_  (
g `  j )
) )
8483imbi2d 309 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) )
85 ssid 3198 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g `
 j )  C_  ( g `  j
)
8685a1ii 26 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  ZZ  ->  (
( A. k  e.  NN  ( g `  ( k  +  1 ) )  C_  (
g `  k )  /\  j  e.  NN )  ->  ( g `  j )  C_  (
g `  j )
) )
87 nnuz 10258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  NN  =  ( ZZ>= `  1 )
8887uztrn2 10240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  e.  NN  /\  m  e.  ( ZZ>= `  j ) )  ->  m  e.  NN )
89 oveq1 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  m  ->  (
k  +  1 )  =  ( m  + 
1 ) )
9089fveq2d 5489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  m  ->  (
g `  ( k  +  1 ) )  =  ( g `  ( m  +  1
) ) )
91 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  =  m  ->  (
g `  k )  =  ( g `  m ) )
9290, 91sseq12d 3208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  =  m  ->  (
( g `  (
k  +  1 ) )  C_  ( g `  k )  <->  ( g `  ( m  +  1 ) )  C_  (
g `  m )
) )
9392rspccva 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A. k  e.  NN  ( g `  (
k  +  1 ) )  C_  ( g `  k )  /\  m  e.  NN )  ->  (
g `  ( m  +  1 ) ) 
C_  ( g `  m ) )
9488, 93sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( A. k  e.  NN  ( g `  (
k  +  1 ) )  C_  ( g `  k )  /\  (
j  e.  NN  /\  m  e.  ( ZZ>= `  j ) ) )  ->  ( g `  ( m  +  1
) )  C_  (
g `  m )
)
9594anassrs 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A. k  e.  NN  ( g `  ( k  +  1 ) )  C_  (
g `  k )  /\  j  e.  NN )  /\  m  e.  (
ZZ>= `  j ) )  ->  ( g `  ( m  +  1
) )  C_  (
g `  m )
)
96 sstr2 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( g `  ( m  +  1 ) ) 
C_  ( g `  m )  ->  (
( g `  m
)  C_  ( g `  j )  ->  (
g `  ( m  +  1 ) ) 
C_  ( g `  j ) ) )
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
) )
9897expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) ) )
9998a2d 25 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) )
10078, 81, 84, 81, 86, 99uzind4 10271 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( ZZ>= `  j
)  ->  ( ( A. k  e.  NN  ( g `  (
k  +  1 ) )  C_  ( g `  k )  /\  j  e.  NN )  ->  (
g `  m )  C_  ( g `  j
) ) )
101100com12 29 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A. k  e.  NN  ( g `  (
k  +  1 ) )  C_  ( g `  k )  /\  j  e.  NN )  ->  (
m  e.  ( ZZ>= `  j )  ->  (
g `  m )  C_  ( g `  j
) ) )
102101ralrimiv 2626 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A. k  e.  NN  ( g `  (
k  +  1 ) )  C_  ( g `  k )  /\  j  e.  NN )  ->  A. m  e.  ( ZZ>= `  j )
( g `  m
)  C_  ( g `  j ) )
10374, 75, 102syl2anc 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 ) )
10475, 88sylan 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( 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 )
105 simplr 734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) )
106105ad2antlr 710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( 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 ) )
107 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  (
f `  n )  =  ( f `  m ) )
108107, 79eleq12d 2352 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( f `  n
)  e.  ( g `
 n )  <->  ( f `  m )  e.  ( g `  m ) ) )
109108rspcv 2881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN  ->  ( A. n  e.  NN  ( f `  n
)  e.  ( g `
 n )  -> 
( f `  m
)  e.  ( g `
 m ) ) )
110104, 106, 109sylc 58 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( 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 ) )
111110ralrimiva 2627 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 ) )
112 r19.26 2676 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
113103, 111, 112sylanbrc 648 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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
) ) )
114 ssel2 3176 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( g `  m
)  C_  ( g `  j )  /\  (
f `  m )  e.  ( g `  m
) )  ->  (
f `  m )  e.  ( g `  j
) )
115114ralimi 2619 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
116113, 115syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 ) )
117 ssel 3175 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g `  j ) 
C_  y  ->  (
( f `  m
)  e.  ( g `
 j )  -> 
( f `  m
)  e.  y ) )
118117ralimdv 2623 . . . . . . . . . . . . . . . . . 18  |-  ( ( g `  j ) 
C_  y  ->  ( A. m  e.  ( ZZ>=
`  j ) ( f `  m )  e.  ( g `  j )  ->  A. m  e.  ( ZZ>= `  j )
( f `  m
)  e.  y ) )
119116, 118syl5com 28 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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 ) )
120119anassrs 632 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 ) )
121120anassrs 632 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( 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 ) )
122121reximdva 2656 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 ) )
12370, 122syld 42 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( 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 ) )
124123ralrimiva 2627 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ) )
12539ad2antrr 709 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 )
1263toptopon 16665 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
127125, 126sylib 190 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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
) )
128 1z 10048 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
129128a1i 12 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
130 simprl 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 )
13138ad2antrr 709 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 )
132 fss 5362 . . . . . . . . . . . . . 14  |-  ( ( f : NN --> S  /\  S  C_  X )  -> 
f : NN --> X )
133130, 131, 132syl2anc 645 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
134 eqidd 2285 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( 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 ) )
135127, 87, 129, 133, 134lmbrf 16984 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ) ) ) )
13659, 124, 135mpbir2and 893 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
137136expr 601 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
138137imdistanda 677 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
13958, 138syland 469 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
140139eximdv 1613 . . . . . . 7  |-  ( ( ( ( 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 ) ) )
14154, 140mpd 16 . . . . . 6  |-  ( ( ( ( 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 ) )
142141ex 425 . . . . 5  |-  ( ( ( 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 ) ) )
143142exlimdv 1668 . . . 4  |-  ( ( ( 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 )
)  ->  E. f
( f : NN --> S  /\  f ( ~~> t `  J ) P ) ) )
1448, 143mpd 16 . . 3  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  P  e.  (
( cls `  J
) `  S )
)  ->  E. f
( f : NN --> S  /\  f ( ~~> t `  J ) P ) )
145144ex 425 . 2  |-  ( ( J  e.  1stc  /\  S  C_  X )  ->  ( P  e.  ( ( cls `  J ) `  S )  ->  E. f
( f : NN --> S  /\  f ( ~~> t `  J ) P ) ) )
1462ad2antrr 709 . . . . . 6  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  J  e.  Top )
147146, 126sylib 190 . . . . 5  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  J  e.  (TopOn `  X ) )
148128a1i 12 . . . . 5  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  1  e.  ZZ )
149 simprr 736 . . . . 5  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  f ( ~~> t `  J ) P )
150 simprl 735 . . . . . 6  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  f : NN
--> S )
151 ffvelrn 5624 . . . . . 6  |-  ( ( f : NN --> S  /\  k  e.  NN )  ->  ( f `  k
)  e.  S )
152150, 151sylan 459 . . . . 5  |-  ( ( ( ( J  e. 
1stc  /\  S  C_  X
)  /\  ( f : NN --> S  /\  f
( ~~> t `  J
) P ) )  /\  k  e.  NN )  ->  ( f `  k )  e.  S
)
153 simplr 734 . . . . 5  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  S  C_  X
)
15487, 147, 148, 149, 152, 153lmcls 17024 . . . 4  |-  ( ( ( J  e.  1stc  /\  S  C_  X )  /\  ( f : NN --> S  /\  f ( ~~> t `  J ) P ) )  ->  P  e.  ( ( cls `  J
) `  S )
)
155154ex 425 . . 3  |-  ( ( J  e.  1stc  /\  S  C_  X )  ->  (
( f : NN --> S  /\  f ( ~~> t `  J ) P )  ->  P  e.  ( ( cls `  J
) `  S )
) )
156155exlimdv 1668 . 2  |-  ( ( J  e.  1stc  /\  S  C_  X )  ->  ( E. f ( f : NN --> S  /\  f
( ~~> t `  J
) P )  ->  P  e.  ( ( cls `  J ) `  S ) ) )
157145, 156impbid 185 1  |-  ( ( J  e.  1stc  /\  S  C_  X )  ->  ( P  e.  ( ( cls `  J ) `  S )  <->  E. f
( f : NN --> S  /\  f ( ~~> t `  J ) P ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 939   E.wex 1533    = wceq 1628    e. wcel 1688    =/= wne 2447   A.wral 2544   E.wrex 2545   _Vcvv 2789    i^i cin 3152    C_ wss 3153   (/)c0 3456   U.cuni 3828   class class class wbr 4024    _I cid 4303   -->wf 5217   ` cfv 5221  (class class class)co 5819   1c1 8733    + caddc 8735   NNcn 9741   ZZcz 10019   ZZ>=cuz 10225   Topctop 16625  TopOnctopon 16626   clsccl 16749   ~~> tclm 16950   1stcc1stc 17157
This theorem is referenced by:  1stccnp  17182  hausmapdom  17220  1stckgen  17243  metelcls  18724
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-13 1690  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-inf2 7337  ax-cc 8056  ax-cnex 8788  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-mulcom 8796  ax-addass 8797  ax-mulass 8798  ax-distr 8799  ax-i2m1 8800  ax-1ne0 8801  ax-1rid 8802  ax-rnegex 8803  ax-rrecex 8804  ax-cnre 8805  ax-pre-lttri 8806  ax-pre-lttrn 8807  ax-pre-ltadd 8808  ax-pre-mulgt0 8809
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5822  df-oprab 5823  df-mpt2 5824  df-1st 6083  df-2nd 6084  df-iota 6252  df-riota 6299  df-recs 6383  df-rdg 6418  df-1o 6474  df-oadd 6478  df-er 6655  df-pm 6770  df-en 6859  df-dom 6860  df-sdom 6861  df-fin 6862  df-pnf 8864  df-mnf 8865  df-xr 8866  df-ltxr 8867  df-le 8868  df-sub 9034  df-neg 9035  df-nn 9742  df-n0 9961  df-z 10020  df-uz 10226  df-fz 10777  df-top 16630  df-topon 16633  df-cld 16750  df-ntr 16751  df-cls 16752  df-lm 16953  df-1stc 17159
  Copyright terms: Public domain W3C validator