MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmcnp Structured version   Visualization version   Unicode version

Theorem lmcnp 20369
Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
Hypotheses
Ref Expression
lmcnp.3  |-  ( ph  ->  F ( ~~> t `  J ) P )
lmcnp.4  |-  ( ph  ->  G  e.  ( ( J  CnP  K ) `
 P ) )
Assertion
Ref Expression
lmcnp  |-  ( ph  ->  ( G  o.  F
) ( ~~> t `  K ) ( G `
 P ) )

Proof of Theorem lmcnp
Dummy variables  j 
k  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmcnp.4 . . . . . 6  |-  ( ph  ->  G  e.  ( ( J  CnP  K ) `
 P ) )
2 eqid 2462 . . . . . . 7  |-  U. J  =  U. J
3 eqid 2462 . . . . . . 7  |-  U. K  =  U. K
42, 3cnpf 20312 . . . . . 6  |-  ( G  e.  ( ( J  CnP  K ) `  P )  ->  G : U. J --> U. K
)
51, 4syl 17 . . . . 5  |-  ( ph  ->  G : U. J --> U. K )
6 lmcnp.3 . . . . . . . . 9  |-  ( ph  ->  F ( ~~> t `  J ) P )
7 cnptop1 20307 . . . . . . . . . . . 12  |-  ( G  e.  ( ( J  CnP  K ) `  P )  ->  J  e.  Top )
81, 7syl 17 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  Top )
92toptopon 19997 . . . . . . . . . . 11  |-  ( J  e.  Top  <->  J  e.  (TopOn `  U. J ) )
108, 9sylib 201 . . . . . . . . . 10  |-  ( ph  ->  J  e.  (TopOn `  U. J ) )
11 nnuz 11223 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
12 1zzd 10997 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ZZ )
1310, 11, 12lmbr2 20324 . . . . . . . . 9  |-  ( ph  ->  ( F ( ~~> t `  J ) P  <->  ( F  e.  ( U. J  ^pm  CC )  /\  P  e. 
U. J  /\  A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) ) ) ) )
146, 13mpbid 215 . . . . . . . 8  |-  ( ph  ->  ( F  e.  ( U. J  ^pm  CC )  /\  P  e.  U. J  /\  A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v ) ) ) )
1514simp1d 1026 . . . . . . 7  |-  ( ph  ->  F  e.  ( U. J  ^pm  CC ) )
16 uniexg 6615 . . . . . . . . 9  |-  ( J  e.  Top  ->  U. J  e.  _V )
178, 16syl 17 . . . . . . . 8  |-  ( ph  ->  U. J  e.  _V )
18 cnex 9646 . . . . . . . 8  |-  CC  e.  _V
19 elpm2g 7514 . . . . . . . 8  |-  ( ( U. J  e.  _V  /\  CC  e.  _V )  ->  ( F  e.  ( U. J  ^pm  CC ) 
<->  ( F : dom  F --> U. J  /\  dom  F 
C_  CC ) ) )
2017, 18, 19sylancl 673 . . . . . . 7  |-  ( ph  ->  ( F  e.  ( U. J  ^pm  CC ) 
<->  ( F : dom  F --> U. J  /\  dom  F 
C_  CC ) ) )
2115, 20mpbid 215 . . . . . 6  |-  ( ph  ->  ( F : dom  F --> U. J  /\  dom  F 
C_  CC ) )
2221simpld 465 . . . . 5  |-  ( ph  ->  F : dom  F --> U. J )
23 fco 5762 . . . . 5  |-  ( ( G : U. J --> U. K  /\  F : dom  F --> U. J )  -> 
( G  o.  F
) : dom  F --> U. K )
245, 22, 23syl2anc 671 . . . 4  |-  ( ph  ->  ( G  o.  F
) : dom  F --> U. K )
25 fdm 5756 . . . . . 6  |-  ( ( G  o.  F ) : dom  F --> U. K  ->  dom  ( G  o.  F )  =  dom  F )
2624, 25syl 17 . . . . 5  |-  ( ph  ->  dom  ( G  o.  F )  =  dom  F )
2726feq2d 5737 . . . 4  |-  ( ph  ->  ( ( G  o.  F ) : dom  ( G  o.  F
) --> U. K  <->  ( G  o.  F ) : dom  F --> U. K ) )
2824, 27mpbird 240 . . 3  |-  ( ph  ->  ( G  o.  F
) : dom  ( G  o.  F ) --> U. K )
2921simprd 469 . . . 4  |-  ( ph  ->  dom  F  C_  CC )
3026, 29eqsstrd 3478 . . 3  |-  ( ph  ->  dom  ( G  o.  F )  C_  CC )
31 cnptop2 20308 . . . . . 6  |-  ( G  e.  ( ( J  CnP  K ) `  P )  ->  K  e.  Top )
321, 31syl 17 . . . . 5  |-  ( ph  ->  K  e.  Top )
33 uniexg 6615 . . . . 5  |-  ( K  e.  Top  ->  U. K  e.  _V )
3432, 33syl 17 . . . 4  |-  ( ph  ->  U. K  e.  _V )
35 elpm2g 7514 . . . 4  |-  ( ( U. K  e.  _V  /\  CC  e.  _V )  ->  ( ( G  o.  F )  e.  ( U. K  ^pm  CC ) 
<->  ( ( G  o.  F ) : dom  ( G  o.  F
) --> U. K  /\  dom  ( G  o.  F
)  C_  CC )
) )
3634, 18, 35sylancl 673 . . 3  |-  ( ph  ->  ( ( G  o.  F )  e.  ( U. K  ^pm  CC ) 
<->  ( ( G  o.  F ) : dom  ( G  o.  F
) --> U. K  /\  dom  ( G  o.  F
)  C_  CC )
) )
3728, 30, 36mpbir2and 938 . 2  |-  ( ph  ->  ( G  o.  F
)  e.  ( U. K  ^pm  CC ) )
3814simp2d 1027 . . 3  |-  ( ph  ->  P  e.  U. J
)
395, 38ffvelrnd 6046 . 2  |-  ( ph  ->  ( G `  P
)  e.  U. K
)
4014simp3d 1028 . . . . . 6  |-  ( ph  ->  A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) ) )
4140adantr 471 . . . . 5  |-  ( (
ph  /\  ( u  e.  K  /\  ( G `  P )  e.  u ) )  ->  A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) ) )
42 cnpimaex 20321 . . . . . . 7  |-  ( ( G  e.  ( ( J  CnP  K ) `
 P )  /\  u  e.  K  /\  ( G `  P )  e.  u )  ->  E. v  e.  J  ( P  e.  v  /\  ( G " v
)  C_  u )
)
43423expb 1216 . . . . . 6  |-  ( ( G  e.  ( ( J  CnP  K ) `
 P )  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( G " v )  C_  u ) )
441, 43sylan 478 . . . . 5  |-  ( (
ph  /\  ( u  e.  K  /\  ( G `  P )  e.  u ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( G " v
)  C_  u )
)
45 r19.29 2937 . . . . . . 7  |-  ( ( A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  /\  E. v  e.  J  ( P  e.  v  /\  ( G
" v )  C_  u ) )  ->  E. v  e.  J  ( ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  /\  ( P  e.  v  /\  ( G " v ) 
C_  u ) ) )
46 pm3.45 850 . . . . . . . . 9  |-  ( ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  ->  ( ( P  e.  v  /\  ( G " v )  C_  u )  ->  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v )  /\  ( G " v ) 
C_  u ) ) )
4746imp 435 . . . . . . . 8  |-  ( ( ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  /\  ( P  e.  v  /\  ( G
" v )  C_  u ) )  -> 
( E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v )  /\  ( G
" v )  C_  u ) )
4847reximi 2867 . . . . . . 7  |-  ( E. v  e.  J  ( ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  /\  ( P  e.  v  /\  ( G
" v )  C_  u ) )  ->  E. v  e.  J  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v )  /\  ( G " v ) 
C_  u ) )
4945, 48syl 17 . . . . . 6  |-  ( ( A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  /\  E. v  e.  J  ( P  e.  v  /\  ( G
" v )  C_  u ) )  ->  E. v  e.  J  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v )  /\  ( G " v ) 
C_  u ) )
505ad3antrrr 741 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  G : U. J
--> U. K )
51 ffn 5751 . . . . . . . . . . . . . . . . . 18  |-  ( G : U. J --> U. K  ->  G  Fn  U. J
)
5250, 51syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  G  Fn  U. J )
53 simplrl 775 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  v  e.  J
)
54 elssuni 4241 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  J  ->  v  C_ 
U. J )
5553, 54syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  v  C_  U. J
)
56 fnfvima 6168 . . . . . . . . . . . . . . . . . 18  |-  ( ( G  Fn  U. J  /\  v  C_  U. J  /\  ( F `  k
)  e.  v )  ->  ( G `  ( F `  k ) )  e.  ( G
" v ) )
57563expia 1217 . . . . . . . . . . . . . . . . 17  |-  ( ( G  Fn  U. J  /\  v  C_  U. J
)  ->  ( ( F `  k )  e.  v  ->  ( G `
 ( F `  k ) )  e.  ( G " v
) ) )
5852, 55, 57syl2anc 671 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( F `
 k )  e.  v  ->  ( G `  ( F `  k
) )  e.  ( G " v ) ) )
5922ad2antrr 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  ( v  e.  J  /\  ( G
" v )  C_  u ) )  ->  F : dom  F --> U. J
)
60 fvco3 5965 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : dom  F --> U. J  /\  k  e.  dom  F )  -> 
( ( G  o.  F ) `  k
)  =  ( G `
 ( F `  k ) ) )
6159, 60sylan 478 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( G  o.  F ) `  k )  =  ( G `  ( F `
 k ) ) )
6261eleq1d 2524 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( ( G  o.  F ) `
 k )  e.  ( G " v
)  <->  ( G `  ( F `  k ) )  e.  ( G
" v ) ) )
6358, 62sylibrd 242 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( F `
 k )  e.  v  ->  ( ( G  o.  F ) `  k )  e.  ( G " v ) ) )
64 simplrr 776 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( G "
v )  C_  u
)
6564sseld 3443 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( ( G  o.  F ) `
 k )  e.  ( G " v
)  ->  ( ( G  o.  F ) `  k )  e.  u
) )
6663, 65syld 45 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( F `
 k )  e.  v  ->  ( ( G  o.  F ) `  k )  e.  u
) )
67 simpr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  k  e.  dom  F )
6826ad3antrrr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  dom  ( G  o.  F )  =  dom  F )
6967, 68eleqtrrd 2543 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  k  e.  dom  ( G  o.  F
) )
7066, 69jctild 550 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( u  e.  K  /\  ( G `  P
)  e.  u ) )  /\  ( v  e.  J  /\  ( G " v )  C_  u ) )  /\  k  e.  dom  F )  ->  ( ( F `
 k )  e.  v  ->  ( k  e.  dom  ( G  o.  F )  /\  (
( G  o.  F
) `  k )  e.  u ) ) )
7170expimpd 612 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  ( v  e.  J  /\  ( G
" v )  C_  u ) )  -> 
( ( k  e. 
dom  F  /\  ( F `  k )  e.  v )  ->  (
k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) )
7271ralimdv 2810 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  ( v  e.  J  /\  ( G
" v )  C_  u ) )  -> 
( A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v )  ->  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  ( G  o.  F
)  /\  ( ( G  o.  F ) `  k )  e.  u
) ) )
7372reximdv 2873 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  ( v  e.  J  /\  ( G
" v )  C_  u ) )  -> 
( E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  ( G  o.  F
)  /\  ( ( G  o.  F ) `  k )  e.  u
) ) )
7473expr 624 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  v  e.  J
)  ->  ( ( G " v )  C_  u  ->  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  ( G  o.  F
)  /\  ( ( G  o.  F ) `  k )  e.  u
) ) ) )
7574com23 81 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  v  e.  J
)  ->  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v )  ->  ( ( G " v )  C_  u  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) ) )
7675impd 437 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  K  /\  ( G `  P )  e.  u ) )  /\  v  e.  J
)  ->  ( ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  F  /\  ( F `  k )  e.  v )  /\  ( G " v ) 
C_  u )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) )
7776rexlimdva 2891 . . . . . 6  |-  ( (
ph  /\  ( u  e.  K  /\  ( G `  P )  e.  u ) )  -> 
( E. v  e.  J  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v )  /\  ( G
" v )  C_  u )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  ( G  o.  F
)  /\  ( ( G  o.  F ) `  k )  e.  u
) ) )
7849, 77syl5 33 . . . . 5  |-  ( (
ph  /\  ( u  e.  K  /\  ( G `  P )  e.  u ) )  -> 
( ( A. v  e.  J  ( P  e.  v  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( k  e.  dom  F  /\  ( F `  k )  e.  v ) )  /\  E. v  e.  J  ( P  e.  v  /\  ( G " v ) 
C_  u ) )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) )
7941, 44, 78mp2and 690 . . . 4  |-  ( (
ph  /\  ( u  e.  K  /\  ( G `  P )  e.  u ) )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) )
8079expr 624 . . 3  |-  ( (
ph  /\  u  e.  K )  ->  (
( G `  P
)  e.  u  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) )
8180ralrimiva 2814 . 2  |-  ( ph  ->  A. u  e.  K  ( ( G `  P )  e.  u  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) )
823toptopon 19997 . . . 4  |-  ( K  e.  Top  <->  K  e.  (TopOn `  U. K ) )
8332, 82sylib 201 . . 3  |-  ( ph  ->  K  e.  (TopOn `  U. K ) )
8483, 11, 12lmbr2 20324 . 2  |-  ( ph  ->  ( ( G  o.  F ) ( ~~> t `  K ) ( G `
 P )  <->  ( ( G  o.  F )  e.  ( U. K  ^pm  CC )  /\  ( G `
 P )  e. 
U. K  /\  A. u  e.  K  (
( G `  P
)  e.  u  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( k  e.  dom  ( G  o.  F )  /\  ( ( G  o.  F ) `  k
)  e.  u ) ) ) ) )
8537, 39, 81, 84mpbir3and 1197 1  |-  ( ph  ->  ( G  o.  F
) ( ~~> t `  K ) ( G `
 P ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898   A.wral 2749   E.wrex 2750   _Vcvv 3057    C_ wss 3416   U.cuni 4212   class class class wbr 4416   dom cdm 4853   "cima 4856    o. ccom 4857    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315    ^pm cpm 7499   CCcc 9563   1c1 9566   NNcn 10637   ZZ>=cuz 11188   Topctop 19966  TopOnctopon 19967    CnP ccnp 20290   ~~> tclm 20291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-map 7500  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-z 10967  df-uz 11189  df-top 19970  df-topon 19972  df-cnp 20293  df-lm 20294
This theorem is referenced by:  lmcn  20370  1stccnp  20526
  Copyright terms: Public domain W3C validator