Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmlift3 Structured version   Unicode version

Theorem cvmlift3 28598
Description: A general version of cvmlift 28569. If  K is simply connected and weakly locally path-connected, then there is a unique lift of functions on  K which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.)
Hypotheses
Ref Expression
cvmlift3.b  |-  B  = 
U. C
cvmlift3.y  |-  Y  = 
U. K
cvmlift3.f  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
cvmlift3.k  |-  ( ph  ->  K  e. SCon )
cvmlift3.l  |-  ( ph  ->  K  e. 𝑛Locally PCon )
cvmlift3.o  |-  ( ph  ->  O  e.  Y )
cvmlift3.g  |-  ( ph  ->  G  e.  ( K  Cn  J ) )
cvmlift3.p  |-  ( ph  ->  P  e.  B )
cvmlift3.e  |-  ( ph  ->  ( F `  P
)  =  ( G `
 O ) )
Assertion
Ref Expression
cvmlift3  |-  ( ph  ->  E! f  e.  ( K  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `  O )  =  P ) )
Distinct variable groups:    f, J    f, F    B, f    f, G    C, f    ph, f    f, K    P, f    f, O   
f, Y

Proof of Theorem cvmlift3
Dummy variables  b 
c  d  k  s  z  g  a  u  v  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmlift3.b . . 3  |-  B  = 
U. C
2 cvmlift3.y . . 3  |-  Y  = 
U. K
3 cvmlift3.f . . 3  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
4 cvmlift3.k . . 3  |-  ( ph  ->  K  e. SCon )
5 cvmlift3.l . . 3  |-  ( ph  ->  K  e. 𝑛Locally PCon )
6 cvmlift3.o . . 3  |-  ( ph  ->  O  e.  Y )
7 cvmlift3.g . . 3  |-  ( ph  ->  G  e.  ( K  Cn  J ) )
8 cvmlift3.p . . 3  |-  ( ph  ->  P  e.  B )
9 cvmlift3.e . . 3  |-  ( ph  ->  ( F `  P
)  =  ( G `
 O ) )
10 eqeq2 2482 . . . . . . . 8  |-  ( b  =  z  ->  (
( ( iota_ d  e.  ( II  Cn  C
) ( ( F  o.  d )  =  ( G  o.  c
)  /\  ( d `  0 )  =  P ) ) ` 
1 )  =  b  <-> 
( ( iota_ d  e.  ( II  Cn  C
) ( ( F  o.  d )  =  ( G  o.  c
)  /\  ( d `  0 )  =  P ) ) ` 
1 )  =  z ) )
11103anbi3d 1305 . . . . . . 7  |-  ( b  =  z  ->  (
( ( c ` 
0 )  =  O  /\  ( c ` 
1 )  =  a  /\  ( ( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  (
d `  0 )  =  P ) ) ` 
1 )  =  b )  <->  ( ( c `
 0 )  =  O  /\  ( c `
 1 )  =  a  /\  ( (
iota_ d  e.  (
II  Cn  C )
( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  z ) ) )
1211rexbidv 2978 . . . . . 6  |-  ( b  =  z  ->  ( E. c  e.  (
II  Cn  K )
( ( c ` 
0 )  =  O  /\  ( c ` 
1 )  =  a  /\  ( ( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  (
d `  0 )  =  P ) ) ` 
1 )  =  b )  <->  E. c  e.  ( II  Cn  K ) ( ( c ` 
0 )  =  O  /\  ( c ` 
1 )  =  a  /\  ( ( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  (
d `  0 )  =  P ) ) ` 
1 )  =  z ) ) )
1312cbvriotav 6267 . . . . 5  |-  ( iota_ b  e.  B  E. c  e.  ( II  Cn  K
) ( ( c `
 0 )  =  O  /\  ( c `
 1 )  =  a  /\  ( (
iota_ d  e.  (
II  Cn  C )
( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  b ) )  =  ( iota_ z  e.  B  E. c  e.  ( II  Cn  K
) ( ( c `
 0 )  =  O  /\  ( c `
 1 )  =  a  /\  ( (
iota_ d  e.  (
II  Cn  C )
( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  z ) )
14 fveq1 5871 . . . . . . . . . 10  |-  ( c  =  f  ->  (
c `  0 )  =  ( f ` 
0 ) )
1514eqeq1d 2469 . . . . . . . . 9  |-  ( c  =  f  ->  (
( c `  0
)  =  O  <->  ( f `  0 )  =  O ) )
16 fveq1 5871 . . . . . . . . . 10  |-  ( c  =  f  ->  (
c `  1 )  =  ( f ` 
1 ) )
1716eqeq1d 2469 . . . . . . . . 9  |-  ( c  =  f  ->  (
( c `  1
)  =  a  <->  ( f `  1 )  =  a ) )
18 coeq2 5167 . . . . . . . . . . . . . . 15  |-  ( d  =  g  ->  ( F  o.  d )  =  ( F  o.  g ) )
1918eqeq1d 2469 . . . . . . . . . . . . . 14  |-  ( d  =  g  ->  (
( F  o.  d
)  =  ( G  o.  c )  <->  ( F  o.  g )  =  ( G  o.  c ) ) )
20 fveq1 5871 . . . . . . . . . . . . . . 15  |-  ( d  =  g  ->  (
d `  0 )  =  ( g ` 
0 ) )
2120eqeq1d 2469 . . . . . . . . . . . . . 14  |-  ( d  =  g  ->  (
( d `  0
)  =  P  <->  ( g `  0 )  =  P ) )
2219, 21anbi12d 710 . . . . . . . . . . . . 13  |-  ( d  =  g  ->  (
( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P )  <->  ( ( F  o.  g )  =  ( G  o.  c
)  /\  ( g `  0 )  =  P ) ) )
2322cbvriotav 6267 . . . . . . . . . . . 12  |-  ( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  (
d `  0 )  =  P ) )  =  ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  c )  /\  ( g ` 
0 )  =  P ) )
24 coeq2 5167 . . . . . . . . . . . . . . 15  |-  ( c  =  f  ->  ( G  o.  c )  =  ( G  o.  f ) )
2524eqeq2d 2481 . . . . . . . . . . . . . 14  |-  ( c  =  f  ->  (
( F  o.  g
)  =  ( G  o.  c )  <->  ( F  o.  g )  =  ( G  o.  f ) ) )
2625anbi1d 704 . . . . . . . . . . . . 13  |-  ( c  =  f  ->  (
( ( F  o.  g )  =  ( G  o.  c )  /\  ( g ` 
0 )  =  P )  <->  ( ( F  o.  g )  =  ( G  o.  f
)  /\  ( g `  0 )  =  P ) ) )
2726riotabidv 6258 . . . . . . . . . . . 12  |-  ( c  =  f  ->  ( iota_ g  e.  ( II 
Cn  C ) ( ( F  o.  g
)  =  ( G  o.  c )  /\  ( g `  0
)  =  P ) )  =  ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) )
2823, 27syl5eq 2520 . . . . . . . . . . 11  |-  ( c  =  f  ->  ( iota_ d  e.  ( II 
Cn  C ) ( ( F  o.  d
)  =  ( G  o.  c )  /\  ( d `  0
)  =  P ) )  =  ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) )
2928fveq1d 5874 . . . . . . . . . 10  |-  ( c  =  f  ->  (
( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  ( (
iota_ g  e.  (
II  Cn  C )
( ( F  o.  g )  =  ( G  o.  f )  /\  ( g ` 
0 )  =  P ) ) `  1
) )
3029eqeq1d 2469 . . . . . . . . 9  |-  ( c  =  f  ->  (
( ( iota_ d  e.  ( II  Cn  C
) ( ( F  o.  d )  =  ( G  o.  c
)  /\  ( d `  0 )  =  P ) ) ` 
1 )  =  z  <-> 
( ( iota_ g  e.  ( II  Cn  C
) ( ( F  o.  g )  =  ( G  o.  f
)  /\  ( g `  0 )  =  P ) ) ` 
1 )  =  z ) )
3115, 17, 303anbi123d 1299 . . . . . . . 8  |-  ( c  =  f  ->  (
( ( c ` 
0 )  =  O  /\  ( c ` 
1 )  =  a  /\  ( ( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  (
d `  0 )  =  P ) ) ` 
1 )  =  z )  <->  ( ( f `
 0 )  =  O  /\  ( f `
 1 )  =  a  /\  ( (
iota_ g  e.  (
II  Cn  C )
( ( F  o.  g )  =  ( G  o.  f )  /\  ( g ` 
0 )  =  P ) ) `  1
)  =  z ) ) )
3231cbvrexv 3094 . . . . . . 7  |-  ( E. c  e.  ( II 
Cn  K ) ( ( c `  0
)  =  O  /\  ( c `  1
)  =  a  /\  ( ( iota_ d  e.  ( II  Cn  C
) ( ( F  o.  d )  =  ( G  o.  c
)  /\  ( d `  0 )  =  P ) ) ` 
1 )  =  z )  <->  E. f  e.  ( II  Cn  K ) ( ( f ` 
0 )  =  O  /\  ( f ` 
1 )  =  a  /\  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) ` 
1 )  =  z ) )
33 eqeq2 2482 . . . . . . . . 9  |-  ( a  =  x  ->  (
( f `  1
)  =  a  <->  ( f `  1 )  =  x ) )
34333anbi2d 1304 . . . . . . . 8  |-  ( a  =  x  ->  (
( ( f ` 
0 )  =  O  /\  ( f ` 
1 )  =  a  /\  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) ` 
1 )  =  z )  <->  ( ( f `
 0 )  =  O  /\  ( f `
 1 )  =  x  /\  ( (
iota_ g  e.  (
II  Cn  C )
( ( F  o.  g )  =  ( G  o.  f )  /\  ( g ` 
0 )  =  P ) ) `  1
)  =  z ) ) )
3534rexbidv 2978 . . . . . . 7  |-  ( a  =  x  ->  ( E. f  e.  (
II  Cn  K )
( ( f ` 
0 )  =  O  /\  ( f ` 
1 )  =  a  /\  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) ` 
1 )  =  z )  <->  E. f  e.  ( II  Cn  K ) ( ( f ` 
0 )  =  O  /\  ( f ` 
1 )  =  x  /\  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) ` 
1 )  =  z ) ) )
3632, 35syl5bb 257 . . . . . 6  |-  ( a  =  x  ->  ( E. c  e.  (
II  Cn  K )
( ( c ` 
0 )  =  O  /\  ( c ` 
1 )  =  a  /\  ( ( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  (
d `  0 )  =  P ) ) ` 
1 )  =  z )  <->  E. f  e.  ( II  Cn  K ) ( ( f ` 
0 )  =  O  /\  ( f ` 
1 )  =  x  /\  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) ` 
1 )  =  z ) ) )
3736riotabidv 6258 . . . . 5  |-  ( a  =  x  ->  ( iota_ z  e.  B  E. c  e.  ( II  Cn  K ) ( ( c `  0 )  =  O  /\  (
c `  1 )  =  a  /\  (
( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  z ) )  =  ( iota_ z  e.  B  E. f  e.  ( II  Cn  K
) ( ( f `
 0 )  =  O  /\  ( f `
 1 )  =  x  /\  ( (
iota_ g  e.  (
II  Cn  C )
( ( F  o.  g )  =  ( G  o.  f )  /\  ( g ` 
0 )  =  P ) ) `  1
)  =  z ) ) )
3813, 37syl5eq 2520 . . . 4  |-  ( a  =  x  ->  ( iota_ b  e.  B  E. c  e.  ( II  Cn  K ) ( ( c `  0 )  =  O  /\  (
c `  1 )  =  a  /\  (
( iota_ d  e.  ( II  Cn  C ) ( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  b ) )  =  ( iota_ z  e.  B  E. f  e.  ( II  Cn  K
) ( ( f `
 0 )  =  O  /\  ( f `
 1 )  =  x  /\  ( (
iota_ g  e.  (
II  Cn  C )
( ( F  o.  g )  =  ( G  o.  f )  /\  ( g ` 
0 )  =  P ) ) `  1
)  =  z ) ) )
3938cbvmptv 4544 . . 3  |-  ( a  e.  Y  |->  ( iota_ b  e.  B  E. c  e.  ( II  Cn  K
) ( ( c `
 0 )  =  O  /\  ( c `
 1 )  =  a  /\  ( (
iota_ d  e.  (
II  Cn  C )
( ( F  o.  d )  =  ( G  o.  c )  /\  ( d ` 
0 )  =  P ) ) `  1
)  =  b ) ) )  =  ( x  e.  Y  |->  (
iota_ z  e.  B  E. f  e.  (
II  Cn  K )
( ( f ` 
0 )  =  O  /\  ( f ` 
1 )  =  x  /\  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  f )  /\  (
g `  0 )  =  P ) ) ` 
1 )  =  z ) ) )
40 eqid 2467 . . . 4  |-  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
k )  /\  A. c  e.  s  ( A. d  e.  (
s  \  { c } ) ( c  i^i  d )  =  (/)  /\  ( F  |`  c )  e.  ( ( Ct  c ) Homeo ( Jt  k ) ) ) ) } )  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " k )  /\  A. c  e.  s  ( A. d  e.  ( s  \  {
c } ) ( c  i^i  d )  =  (/)  /\  ( F  |`  c )  e.  ( ( Ct  c )
Homeo ( Jt  k ) ) ) ) } )
4140cvmscbv 28528 . . 3  |-  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
k )  /\  A. c  e.  s  ( A. d  e.  (
s  \  { c } ) ( c  i^i  d )  =  (/)  /\  ( F  |`  c )  e.  ( ( Ct  c ) Homeo ( Jt  k ) ) ) ) } )  =  ( a  e.  J  |->  { b  e.  ( ~P C  \  { (/)
} )  |  ( U. b  =  ( `' F " a )  /\  A. v  e.  b  ( A. u  e.  ( b  \  {
v } ) ( v  i^i  u )  =  (/)  /\  ( F  |`  v )  e.  ( ( Ct  v )
Homeo ( Jt  a ) ) ) ) } )
421, 2, 3, 4, 5, 6, 7, 8, 9, 39, 41cvmlift3lem9 28597 . 2  |-  ( ph  ->  E. f  e.  ( K  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `  O )  =  P ) )
43 sconpcon 28497 . . . 4  |-  ( K  e. SCon  ->  K  e. PCon )
44 pconcon 28501 . . . 4  |-  ( K  e. PCon  ->  K  e.  Con )
454, 43, 443syl 20 . . 3  |-  ( ph  ->  K  e.  Con )
46 pconcon 28501 . . . . . 6  |-  ( x  e. PCon  ->  x  e.  Con )
4746ssriv 3513 . . . . 5  |- PCon  C_  Con
48 nllyss 19849 . . . . 5  |-  (PCon  C_  Con  -> 𝑛Locally PCon  C_ 𝑛Locally  Con )
4947, 48ax-mp 5 . . . 4  |- 𝑛Locally PCon  C_ 𝑛Locally  Con
5049, 5sseldi 3507 . . 3  |-  ( ph  ->  K  e. 𝑛Locally  Con )
511, 2, 3, 45, 50, 6, 7, 8, 9cvmliftmo 28554 . 2  |-  ( ph  ->  E* f  e.  ( K  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `  O )  =  P ) )
52 reu5 3082 . 2  |-  ( E! f  e.  ( K  Cn  C ) ( ( F  o.  f
)  =  G  /\  ( f `  O
)  =  P )  <-> 
( E. f  e.  ( K  Cn  C
) ( ( F  o.  f )  =  G  /\  ( f `
 O )  =  P )  /\  E* f  e.  ( K  Cn  C ) ( ( F  o.  f )  =  G  /\  (
f `  O )  =  P ) ) )
5342, 51, 52sylanbrc 664 1  |-  ( ph  ->  E! f  e.  ( K  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `  O )  =  P ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818   E!wreu 2819   E*wrmo 2820   {crab 2821    \ cdif 3478    i^i cin 3480    C_ wss 3481   (/)c0 3790   ~Pcpw 4016   {csn 4033   U.cuni 4251    |-> cmpt 4511   `'ccnv 5004    |` cres 5007   "cima 5008    o. ccom 5009   ` cfv 5594   iota_crio 6255  (class class class)co 6295   0cc0 9504   1c1 9505   ↾t crest 14693    Cn ccn 19593   Conccon 19780  𝑛Locally cnlly 19834   Homeochmeo 20122   IIcii 21247  PConcpcon 28489  SConcscon 28490   CovMap ccvm 28525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-er 7323  df-ec 7325  df-map 7434  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-clim 13291  df-sum 13489  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-cn 19596  df-cnp 19597  df-cmp 19755  df-con 19781  df-lly 19835  df-nlly 19836  df-tx 19931  df-hmeo 20124  df-xms 20691  df-ms 20692  df-tms 20693  df-ii 21249  df-htpy 21338  df-phtpy 21339  df-phtpc 21360  df-pco 21373  df-pcon 28491  df-scon 28492  df-cvm 28526
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator