HomeHome Metamath Proof Explorer
Theorem List (p. 232 of 313)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21423)
  Hilbert Space Explorer  Hilbert Space Explorer
(21424-22946)
  Users' Mathboxes  Users' Mathboxes
(22947-31284)
 

Theorem List for Metamath Proof Explorer - 23101-23200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremptpcon 23101 The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015.)
 |-  (
 ( A  e.  V  /\  F : A -->PCon )  ->  ( Xt_ `  F )  e. PCon )
 
Theoremindispcon 23102 The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 14-Aug-2015.)
 |-  { (/) ,  A }  e. PCon
 
Theoremconpcon 23103 A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.)
 |-  (
 ( J  e.  Con  /\  J  e. 𝑛Locally PCon )  ->  J  e. PCon )
 
Theoremqtoppcon 23104 A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
 |-  X  =  U. J   =>    |-  ( ( J  e. PCon  /\  F  Fn  X ) 
 ->  ( J qTop  F )  e. PCon )
 
Theorempconpi1 23105 All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  X  =  U. J   &    |-  P  =  ( J  pi 1  A )   &    |-  Q  =  ( J  pi 1  B )   &    |-  S  =  ( Base `  P )   &    |-  T  =  (
 Base `  Q )   =>    |-  ( ( J  e. PCon  /\  A  e.  X  /\  B  e.  X )  ->  P  ~=ph𝑔 
 Q )
 
Theoremsconpht2 23106 Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  ( ph  ->  J  e. SCon )   &    |-  ( ph  ->  F  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  ( F `  0 )  =  ( G `  0 ) )   &    |-  ( ph  ->  ( F `  1 )  =  ( G `  1 ) )   =>    |-  ( ph  ->  F (  ~=ph  `  J ) G )
 
Theoremsconpi1 23107 A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  X  =  U. J   =>    |-  ( ( J  e. PCon  /\  Y  e.  X ) 
 ->  ( J  e. SCon  <->  ( Base `  ( J  pi 1  Y ) )  ~~  1o )
 )
 
Theoremtxsconlem 23108 Lemma for txscon 23109. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  ( ph  ->  R  e.  Top )   &    |-  ( ph  ->  S  e.  Top )   &    |-  ( ph  ->  F  e.  ( II  Cn  ( R  tX  S ) ) )   &    |-  A  =  ( ( 1st  |`  ( U. R  X.  U. S ) )  o.  F )   &    |-  B  =  ( ( 2nd  |`  ( U. R  X.  U. S ) )  o.  F )   &    |-  ( ph  ->  G  e.  ( A ( PHtpy `  R ) ( ( 0 [,] 1 )  X.  { ( A `  0
 ) } ) ) )   &    |-  ( ph  ->  H  e.  ( B (
 PHtpy `  S ) ( ( 0 [,] 1
 )  X.  { ( B `  0 ) }
 ) ) )   =>    |-  ( ph  ->  F (  ~=ph  `  ( R  tX  S ) ) ( ( 0 [,] 1
 )  X.  { ( F `  0 ) }
 ) )
 
Theoremtxscon 23109 The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  (
 ( R  e. SCon  /\  S  e. SCon )  ->  ( R  tX  S )  e. SCon )
 
Theoremcvxpcon 23110* A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  ( ph  ->  S  C_  CC )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  t  e.  ( 0 [,] 1 ) ) ) 
 ->  ( ( t  x.  x )  +  (
 ( 1  -  t
 )  x.  y ) )  e.  S )   &    |-  J  =  ( TopOpen ` fld )   &    |-  K  =  ( Jt  S )   =>    |-  ( ph  ->  K  e. PCon )
 
Theoremcvxscon 23111* A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  ( ph  ->  S  C_  CC )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  t  e.  ( 0 [,] 1 ) ) ) 
 ->  ( ( t  x.  x )  +  (
 ( 1  -  t
 )  x.  y ) )  e.  S )   &    |-  J  =  ( TopOpen ` fld )   &    |-  K  =  ( Jt  S )   =>    |-  ( ph  ->  K  e. SCon )
 
Theoremblscon 23112 An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
 |-  J  =  ( TopOpen ` fld )   &    |-  S  =  ( P ( ball `  ( abs  o.  -  ) ) R )   &    |-  K  =  ( Jt  S )   =>    |-  ( ( P  e.  CC  /\  R  e.  RR* )  ->  K  e. SCon )
 
Theoremcnllyscon 23113 The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.)
 |-  J  =  ( TopOpen ` fld )   =>    |-  J  e. Locally SCon
 
Theoremrescon 23114 A subset of  RR is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  J  =  ( ( topGen `  ran  (,) )t  A )   =>    |-  ( A  C_  RR  ->  ( J  e. SCon  <->  J  e.  Con ) )
 
Theoremiooscon 23115 An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  (
 ( topGen `  ran  (,) )t  ( A (,) B ) )  e. SCon
 
Theoremiccscon 23116 An closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( ( topGen `  ran  (,) )t  ( A [,] B ) )  e. SCon )
 
Theoremretopscon 23117 The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  ( topGen `
  ran  (,) )  e. SCon
 
Theoremiccllyscon 23118 An closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( ( topGen `  ran  (,) )t  ( A [,] B ) )  e. Locally SCon )
 
Theoremrellyscon 23119 The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  ( topGen `
  ran  (,) )  e. Locally SCon
 
Theoremiiscon 23120 The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  II  e. SCon
 
Theoremiillyscon 23121 The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  II  e. Locally SCon
 
Theoremiinllycon 23122 The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  II  e. 𝑛Locally  Con
 
16.4.9  Covering maps
 
Syntaxccvm 23123 Extend class notation with the class of covering maps.
 class CovMap
 
Definitiondf-cvm 23124* Define the class of covering maps on two topological spaces. A function  f : c --> j is a covering map if it is continuous and for every point  x in the target space there is a neighborhood 
k of  x and a decomposition  s of the preimage of  k as a disjoint union such that  f is a homeomorphism of each set  u  e.  s onto  k. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |- CovMap  =  ( c  e.  Top ,  j  e.  Top  |->  { f  e.  ( c  Cn  j
 )  |  A. x  e.  U. j E. k  e.  j  ( x  e.  k  /\  E. s  e.  ( ~P c  \  { (/) } ) (
 U. s  =  ( `' f " k ) 
 /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( f  |`  u )  e.  (
 ( ct  u )  Homeo  ( jt  k ) ) ) ) ) } )
 
Theoremfncvm 23125 Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |- CovMap  Fn  ( Top  X.  Top )
 
Theoremcvmscbv 23126* Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  S  =  ( a  e.  J  |->  { b  e.  ( ~P C  \  { (/) } )  |  ( U. b  =  ( `' F "
 a )  /\  A. c  e.  b  ( A. d  e.  (
 b  \  { c } ) ( c  i^i  d )  =  (/)  /\  ( F  |`  c )  e.  ( ( Ct  c )  Homeo  ( Jt  a ) ) ) ) }
 )
 
Theoremiscvm 23127* The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  X  =  U. J   =>    |-  ( F  e.  ( C CovMap  J )  <->  ( ( C  e.  Top  /\  J  e.  Top  /\  F  e.  ( C  Cn  J ) ) 
 /\  A. x  e.  X  E. k  e.  J  ( x  e.  k  /\  ( S `  k
 )  =/=  (/) ) ) )
 
Theoremcvmtop1 23128 Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
 |-  ( F  e.  ( C CovMap  J )  ->  C  e.  Top )
 
Theoremcvmtop2 23129 Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  ( F  e.  ( C CovMap  J )  ->  J  e.  Top )
 
Theoremcvmcn 23130 A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  ( F  e.  ( C CovMap  J )  ->  F  e.  ( C  Cn  J ) )
 
Theoremcvmcov 23131* Property of a covering map. In order to make the covering property more manageable, we define here the set  S ( k ) of all even coverings of an open set  k in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  X  =  U. J   =>    |-  (
 ( F  e.  ( C CovMap  J )  /\  P  e.  X )  ->  E. x  e.  J  ( P  e.  x  /\  ( S `  x )  =/=  (/) ) )
 
Theoremcvmsrcl 23132* Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( T  e.  ( S `  U )  ->  U  e.  J )
 
Theoremcvmsi 23133* One direction of cvmsval 23134. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( T  e.  ( S `  U )  ->  ( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U ) 
 /\  A. u  e.  T  ( A. v  e.  ( T  \  { u }
 ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
 Homeo  ( Jt  U ) ) ) ) ) )
 
Theoremcvmsval 23134* Elementhood in the set  S of all even coverings of an open set in  J.  S is an even covering of  U if it is a nonempty collection of disjoint open sets in  C whose union is the preimage of  U, such that each set  u  e.  S is homeomorphic under  F to  U. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( C  e.  V  ->  ( T  e.  ( S `  U )  <->  ( U  e.  J  /\  ( T  C_  C  /\  T  =/=  (/) )  /\  ( U. T  =  ( `' F " U ) 
 /\  A. u  e.  T  ( A. v  e.  ( T  \  { u }
 ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u ) 
 Homeo  ( Jt  U ) ) ) ) ) ) )
 
Theoremcvmsss 23135* An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (Contributed by Mario Carneiro, 11-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( T  e.  ( S `  U )  ->  T  C_  C )
 
Theoremcvmsn0 23136* An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( T  e.  ( S `  U )  ->  T  =/=  (/) )
 
Theoremcvmsuni 23137* An even covering of  U has union equal to the preimage of 
U by  F. (Contributed by Mario Carneiro, 11-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( T  e.  ( S `  U )  ->  U. T  =  ( `' F " U ) )
 
Theoremcvmsdisj 23138* An even covering of  U is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ( T  e.  ( S `  U ) 
 /\  A  e.  T  /\  B  e.  T ) 
 ->  ( A  =  B  \/  ( A  i^i  B )  =  (/) ) )
 
Theoremcvmshmeo 23139* Every element of an even covering of  U is homeomorphic to  U via  F. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ( T  e.  ( S `  U ) 
 /\  A  e.  T )  ->  ( F  |`  A )  e.  ( ( Ct  A )  Homeo  ( Jt  U ) ) )
 
Theoremcvmsf1o 23140*  F, localized to an element of an even covering of  U, is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ( F  e.  ( C CovMap  J )  /\  T  e.  ( S `  U )  /\  A  e.  T )  ->  ( F  |`  A ) : A -1-1-onto-> U )
 
Theoremcvmscld 23141* The sets of an even covering are clopen in the subspace topology on  T. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ( F  e.  ( C CovMap  J )  /\  T  e.  ( S `  U )  /\  A  e.  T )  ->  A  e.  ( Clsd `  ( Ct  ( `' F " U ) ) ) )
 
Theoremcvmsss2 23142* An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ( F  e.  ( C CovMap  J )  /\  V  e.  J  /\  V  C_  U )  ->  ( ( S `  U )  =/=  (/)  ->  ( S `  V )  =/=  (/) ) )
 
Theoremcvmcov2 23143* The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ( F  e.  ( C CovMap  J )  /\  U  e.  J  /\  P  e.  U )  ->  E. x  e.  ~P  U ( P  e.  x  /\  ( S `  x )  =/=  (/) ) )
 
Theoremcvmseu 23144* Every element in  U. T is a member of a unique element of  T. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   =>    |-  (
 ( F  e.  ( C CovMap  J )  /\  ( T  e.  ( S `  U )  /\  A  e.  B  /\  ( F `
  A )  e.  U ) )  ->  E! x  e.  T  A  e.  x )
 
Theoremcvmsiota 23145* Identify the unique element of  T containing  A. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  W  =  ( iota_ x  e.  T A  e.  x )   =>    |-  (
 ( F  e.  ( C CovMap  J )  /\  ( T  e.  ( S `  U )  /\  A  e.  B  /\  ( F `
  A )  e.  U ) )  ->  ( W  e.  T  /\  A  e.  W ) )
 
Theoremcvmopnlem 23146* Lemma for cvmopn 23148. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   =>    |-  (
 ( F  e.  ( C CovMap  J )  /\  A  e.  C )  ->  ( F " A )  e.  J )
 
Theoremcvmfolem 23147* Lemma for cvmfo 23168. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   =>    |-  ( F  e.  ( C CovMap  J )  ->  F : B -onto-> X )
 
Theoremcvmopn 23148 A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  (
 ( F  e.  ( C CovMap  J )  /\  A  e.  C )  ->  ( F " A )  e.  J )
 
Theoremcvmliftmolem1 23149* Lemma for cvmliftmo 23152. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e.  Con )   &    |-  ( ph  ->  K  e. 𝑛Locally  Con )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  M  e.  ( K  Cn  C ) )   &    |-  ( ph  ->  N  e.  ( K  Cn  C ) )   &    |-  ( ph  ->  ( F  o.  M )  =  ( F  o.  N ) )   &    |-  ( ph  ->  ( M `  O )  =  ( N `  O ) )   &    |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  ( ( ph  /\  ps )  ->  T  e.  ( S `  U ) )   &    |-  ( ( ph  /\  ps )  ->  W  e.  T )   &    |-  ( ( ph  /\  ps )  ->  I  C_  ( `' M " W ) )   &    |-  ( ( ph  /\ 
 ps )  ->  ( Kt  I )  e.  Con )   &    |-  ( ( ph  /\  ps )  ->  X  e.  I
 )   &    |-  ( ( ph  /\  ps )  ->  Q  e.  I
 )   &    |-  ( ( ph  /\  ps )  ->  R  e.  I
 )   &    |-  ( ( ph  /\  ps )  ->  ( F `  ( M `  X ) )  e.  U )   =>    |-  ( ( ph  /\  ps )  ->  ( Q  e.  dom  (  M  i^i  N )  ->  R  e.  dom  (  M  i^i  N ) ) )
 
Theoremcvmliftmolem2 23150* Lemma for cvmliftmo 23152. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e.  Con )   &    |-  ( ph  ->  K  e. 𝑛Locally  Con )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  M  e.  ( K  Cn  C ) )   &    |-  ( ph  ->  N  e.  ( K  Cn  C ) )   &    |-  ( ph  ->  ( F  o.  M )  =  ( F  o.  N ) )   &    |-  ( ph  ->  ( M `  O )  =  ( N `  O ) )   &    |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   =>    |-  ( ph  ->  M  =  N )
 
Theoremcvmliftmoi 23151 A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e.  Con )   &    |-  ( ph  ->  K  e. 𝑛Locally  Con )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  M  e.  ( K  Cn  C ) )   &    |-  ( ph  ->  N  e.  ( K  Cn  C ) )   &    |-  ( ph  ->  ( F  o.  M )  =  ( F  o.  N ) )   &    |-  ( ph  ->  ( M `  O )  =  ( N `  O ) )   =>    |-  ( ph  ->  M  =  N )
 
Theoremcvmliftmo 23152* A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e.  Con )   &    |-  ( ph  ->  K  e. 𝑛Locally  Con )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   =>    |-  ( ph  ->  E* f ( f  e.  ( K  Cn  C )  /\  ( ( F  o.  f )  =  G  /\  ( f `
  O )  =  P ) ) )
 
Theoremcvmliftlem1 23153* Lemma for cvmlift 23167. In cvmliftlem15 23166, we picked an  N large enough so that the sections  ( G " [ ( k  -  1 )  /  N ,  k  /  N ] ) are all contained in an even covering, and the function  T enumerates these even coverings. So  1st `  ( T `  M
) is a neighborhood of  ( G " [
( M  -  1 )  /  N ,  M  /  N ] ), and  2nd `  ( T `  M ) is an even covering of  1st `  ( T `  M ), which is to say a disjoint union of open sets in  C whose image is  1st `  ( T `
 M ). (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  ( ( ph  /\ 
 ps )  ->  M  e.  ( 1 ... N ) )   =>    |-  ( ( ph  /\  ps )  ->  ( 2nd `  ( T `  M ) )  e.  ( S `  ( 1st `  ( T `  M ) ) ) )
 
Theoremcvmliftlem2 23154* Lemma for cvmlift 23167. 
W  =  [ ( k  -  1 )  /  N ,  k  /  N ] is a subset of  [ 0 ,  1 ] for each  M  e.  ( 1 ... N
). (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  ( ( ph  /\ 
 ps )  ->  M  e.  ( 1 ... N ) )   &    |-  W  =  ( ( ( M  -  1 )  /  N ) [,] ( M  /  N ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  W  C_  ( 0 [,] 1
 ) )
 
Theoremcvmliftlem3 23155* Lemma for cvmlift 23167. Since  1st `  ( T `  M
) is a neighborhood of  ( G " W ), every element  A  e.  W satisfies  ( G `  A )  e.  ( 1st `  ( T `
 M ) ). (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  ( ( ph  /\ 
 ps )  ->  M  e.  ( 1 ... N ) )   &    |-  W  =  ( ( ( M  -  1 )  /  N ) [,] ( M  /  N ) )   &    |-  (
 ( ph  /\  ps )  ->  A  e.  W )   =>    |-  ( ( ph  /\  ps )  ->  ( G `  A )  e.  ( 1st `  ( T `  M ) ) )
 
Theoremcvmliftlem4 23156* Lemma for cvmlift 23167. The function  Q will be our lifted path, defined piecewise on each section  [ ( M  -  1 )  /  N ,  M  /  N ] for  M  e.  ( 1 ... N ). For 
M  =  0, it is a "seed" value which makes the rest of the recursion work, a singleton function mapping  0 to  P. (Contributed by Mario Carneiro, 15-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   =>    |-  ( Q `  0 )  =  { <. 0 ,  P >. }
 
Theoremcvmliftlem5 23157* Lemma for cvmlift 23167. Definition of  Q at a successor. This is a function defined on  W as  `' ( T  |`  I )  o.  G where  I is the unique covering set of  2nd `  ( T `  M ) that contains  Q ( M  -  1 ) evaluated at the last defined point, namely  ( M  - 
1 )  /  N (note that for  M  =  1 this is using the seed value  Q ( 0 ) ( 0 )  =  P). (Contributed by Mario Carneiro, 15-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  W  =  ( ( ( M  -  1 )  /  N ) [,] ( M  /  N ) )   =>    |-  ( ( ph  /\  M  e.  NN )  ->  ( Q `  M )  =  ( z  e.  W  |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  M ) ) ( ( Q `  ( M  -  1
 ) ) `  (
 ( M  -  1
 )  /  N )
 )  e.  b ) ) `  ( G `
  z ) ) ) )
 
Theoremcvmliftlem6 23158* Lemma for cvmlift 23167. Induction step for cvmliftlem7 23159. Assuming that  Q ( M  - 
1 ) is defined at  ( M  -  1 )  /  N and is a preimage of  G ( ( M  -  1 )  /  N ), the next segment  Q ( M ) is also defined and is a function on  W which is a lift  G for this segment. This follows explicitly from the definition  Q ( M )  =  `' ( F  |`  I )  o.  G since  G is in  1st `  ( F `  M ) for the entire interval so that  `' ( F  |`  I ) maps this into  I and  F  o.  Q maps back to  G. (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  W  =  ( ( ( M  -  1 )  /  N ) [,] ( M  /  N ) )   &    |-  ( ( ph  /\  ps )  ->  M  e.  (
 1 ... N ) )   &    |-  ( ( ph  /\  ps )  ->  ( ( Q `
  ( M  -  1 ) ) `  ( ( M  -  1 )  /  N ) )  e.  ( `' F " { ( G `  ( ( M  -  1 )  /  N ) ) }
 ) )   =>    |-  ( ( ph  /\  ps )  ->  ( ( Q `
  M ) : W --> B  /\  ( F  o.  ( Q `  M ) )  =  ( G  |`  W ) ) )
 
Theoremcvmliftlem7 23159* Lemma for cvmlift 23167. Prove by induction that every  Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 23158 to show functionality and lifting of  Q). (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  W  =  ( ( ( M  -  1 )  /  N ) [,] ( M  /  N ) )   =>    |-  ( ( ph  /\  M  e.  ( 1 ... N ) )  ->  ( ( Q `  ( M  -  1 ) ) `
  ( ( M  -  1 )  /  N ) )  e.  ( `' F " { ( G `  ( ( M  -  1 )  /  N ) ) } ) )
 
Theoremcvmliftlem8 23160* Lemma for cvmlift 23167. The functions  Q are continuous functions because they are defined as  `' ( F  |`  I )  o.  G where  G is continuous and  ( F  |`  I ) is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  W  =  ( ( ( M  -  1 )  /  N ) [,] ( M  /  N ) )   =>    |-  ( ( ph  /\  M  e.  ( 1 ... N ) )  ->  ( Q `
  M )  e.  ( ( Lt  W )  Cn  C ) )
 
Theoremcvmliftlem9 23161* Lemma for cvmlift 23167. The  Q ( M ) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the  Q functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   =>    |-  ( ( ph  /\  M  e.  ( 1
 ... N ) ) 
 ->  ( ( Q `  M ) `  (
 ( M  -  1
 )  /  N )
 )  =  ( ( Q `  ( M  -  1 ) ) `
  ( ( M  -  1 )  /  N ) ) )
 
Theoremcvmliftlem10 23162* Lemma for cvmlift 23167. The function  K is going to be our complete lifted path, formed by unioning together all the  Q functions (each of which is defined on one segment  [ ( M  -  1 )  /  N ,  M  /  N ] of the interval). Here we prove by induction that  K is a continuous function and a lift of  G by applying cvmliftlem6 23158, cvmliftlem7 23159 (to show it is a function and a lift), cvmliftlem8 23160 (to show it is continuous), and cvmliftlem9 23161 (to show that different 
Q functions agree on the intersection of their domains, so that the pasting lemma paste 16949 gives that  K is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  K  =  U_ k  e.  (
 1 ... N ) ( Q `  k )   &    |-  ( ch  <->  ( ( n  e.  NN  /\  ( n  +  1 )  e.  ( 1 ... N ) )  /\  ( U_ k  e.  ( 1 ... n ) ( Q `
  k )  e.  ( ( Lt  ( 0 [,] ( n  /  N ) ) )  Cn  C )  /\  ( F  o.  U_ k  e.  ( 1 ... n ) ( Q `  k ) )  =  ( G  |`  ( 0 [,] ( n  /  N ) ) ) ) ) )   =>    |-  ( ph  ->  ( K  e.  ( ( Lt  ( 0 [,] ( N  /  N ) ) )  Cn  C ) 
 /\  ( F  o.  K )  =  ( G  |`  ( 0 [,] ( N  /  N ) ) ) ) )
 
Theoremcvmliftlem11 23163* Lemma for cvmlift 23167. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  K  =  U_ k  e.  (
 1 ... N ) ( Q `  k )   =>    |-  ( ph  ->  ( K  e.  ( II  Cn  C )  /\  ( F  o.  K )  =  G ) )
 
Theoremcvmliftlem13 23164* Lemma for cvmlift 23167. The initial value of  K is  P because  Q ( 1 ) is a subset of  K which takes value  P at  0. (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  K  =  U_ k  e.  (
 1 ... N ) ( Q `  k )   =>    |-  ( ph  ->  ( K `  0 )  =  P )
 
Theoremcvmliftlem14 23165* Lemma for cvmlift 23167. Putting the results of cvmliftlem11 23163, cvmliftlem13 23164 and cvmliftmo 23152 together, we have that  K is a continuous function, satisfies  F  o.  K  =  G and  K ( 0 )  =  P, and is equal to any other function which also has these properties, so it follows that  K is the unique lift of  G. (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  T : ( 1 ... N ) -->
 U_ j  e.  J  ( { j }  X.  ( S `  j ) ) )   &    |-  ( ph  ->  A. k  e.  ( 1
 ... N ) ( G " ( ( ( k  -  1
 )  /  N ) [,] ( k  /  N ) ) )  C_  ( 1st `  ( T `  k ) ) )   &    |-  L  =  ( topGen `  ran  (,) )   &    |-  Q  =  seq  0 ( ( x  e.  _V ,  m  e.  NN  |->  ( z  e.  ( ( ( m  -  1 )  /  N ) [,] ( m  /  N ) ) 
 |->  ( `' ( F  |`  ( iota_ b  e.  ( 2nd `  ( T `  m ) ) ( x `  ( ( m  -  1 ) 
 /  N ) )  e.  b ) ) `
  ( G `  z ) ) ) ) ,  ( (  _I  |`  NN )  u.  { <. 0 ,  { <. 0 ,  P >. }
 >. } ) )   &    |-  K  =  U_ k  e.  (
 1 ... N ) ( Q `  k )   =>    |-  ( ph  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `
  0 )  =  P ) )
 
Theoremcvmliftlem15 23166* Lemma for cvmlift 23167. Discharge the assumptions of cvmliftlem14 23165. The set of all open subsets 
u of the unit interval such that  G " u is contained in an even covering of some open set in  J is a cover of  II by the definition of a covering map, so by the Lebesgue number lemma lebnumii 18391, there is a subdivision of the unit interval into  N equal parts such that each part is entirely contained within one such open set of  J. Then using finite choice ac6sfi 7034 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 23165. (Contributed by Mario Carneiro, 14-Feb-2015.)
 |-  S  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
 k )  /\  A. u  e.  s  ( A. v  e.  (
 s  \  { u } ) ( u  i^i  v )  =  (/)  /\  ( F  |`  u )  e.  ( ( Ct  u )  Homeo  ( Jt  k ) ) ) ) }
 )   &    |-  B  =  U. C   &    |-  X  =  U. J   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   =>    |-  ( ph  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  (
 f `  0 )  =  P ) )
 
Theoremcvmlift 23167* One of the important properties of covering maps is that any path  G in the base space "lifts" to a path  f in the covering space such that  F  o.  f  =  G, and given a starting point  P in the covering space this lift is unique. The proof is contained in cvmliftlem1 23153 thru cvmliftlem15 23166. (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  B  =  U. C   =>    |-  ( ( ( F  e.  ( C CovMap  J )  /\  G  e.  ( II  Cn  J ) ) 
 /\  ( P  e.  B  /\  ( F `  P )  =  ( G `  0 ) ) )  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `
  0 )  =  P ) )
 
Theoremcvmfo 23168 A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  B  =  U. C   &    |-  X  =  U. J   =>    |-  ( F  e.  ( C CovMap  J )  ->  F : B -onto-> X )
 
Theoremcvmliftiota 23169* Write out a function  H that is the unique lift of  F. (Contributed by Mario Carneiro, 16-Feb-2015.)
 |-  B  =  U. C   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  0
 )  =  P ) )   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0
 ) )   =>    |-  ( ph  ->  ( H  e.  ( II  Cn  C )  /\  ( F  o.  H )  =  G  /\  ( H `
  0 )  =  P ) )
 
Theoremcvmlift2lem1 23170* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  ( A. y  e.  (
 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `  { y } )
 ( ( u  X.  { x } )  C_  M 
 <->  ( u  X.  {
 t } )  C_  M )  ->  ( ( ( 0 [,] 1
 )  X.  { x } )  C_  M  ->  ( ( 0 [,] 1
 )  X.  { t } )  C_  M ) )
 
Theoremcvmlift2lem9a 23171* Lemma for cvmlift2 23184 and cvmlift3 23196. (Contributed by Mario Carneiro, 9-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  S  =  ( 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 ) ) ) ) }
 )   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  H : Y --> B )   &    |-  ( ph  ->  ( F  o.  H )  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  K  e.  Top )   &    |-  ( ph  ->  X  e.  Y )   &    |-  ( ph  ->  T  e.  ( S `  A ) )   &    |-  ( ph  ->  ( W  e.  T  /\  ( H `
  X )  e.  W ) )   &    |-  ( ph  ->  M  C_  Y )   &    |-  ( ph  ->  ( H " M )  C_  W )   =>    |-  ( ph  ->  ( H  |`  M )  e.  ( ( Kt  M )  Cn  C ) )
 
Theoremcvmlift2lem2 23172* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   =>    |-  ( ph  ->  ( H  e.  ( II  Cn  C )  /\  ( F  o.  H )  =  ( z  e.  (
 0 [,] 1 )  |->  ( z G 0 ) )  /\  ( H `
  0 )  =  P ) )
 
Theoremcvmlift2lem3 23173* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( X G z ) ) 
 /\  ( f `  0 )  =  ( H `  X ) ) )   =>    |-  ( ( ph  /\  X  e.  ( 0 [,] 1
 ) )  ->  ( K  e.  ( II  Cn  C )  /\  ( F  o.  K )  =  ( z  e.  (
 0 [,] 1 )  |->  ( X G z ) )  /\  ( K `
  0 )  =  ( H `  X ) ) )
 
Theoremcvmlift2lem4 23174* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   =>    |-  ( ( X  e.  ( 0 [,] 1
 )  /\  Y  e.  ( 0 [,] 1
 ) )  ->  ( X K Y )  =  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  ( z  e.  (
 0 [,] 1 )  |->  ( X G z ) )  /\  ( f `
  0 )  =  ( H `  X ) ) ) `  Y ) )
 
Theoremcvmlift2lem5 23175* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   =>    |-  ( ph  ->  K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1
 ) ) --> B )
 
Theoremcvmlift2lem6 23176* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   =>    |-  ( ( ph  /\  X  e.  ( 0 [,] 1
 ) )  ->  ( K  |`  ( { X }  X.  ( 0 [,] 1 ) ) )  e.  ( ( ( II  tX  II )t  ( { X }  X.  (
 0 [,] 1 ) ) )  Cn  C ) )
 
Theoremcvmlift2lem7 23177* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   =>    |-  ( ph  ->  ( F  o.  K )  =  G )
 
Theoremcvmlift2lem8 23178* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 9-Mar-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   =>    |-  ( ( ph  /\  X  e.  ( 0 [,] 1
 ) )  ->  ( X K 0 )  =  ( H `  X ) )
 
Theoremcvmlift2lem9 23179* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   &    |-  S  =  ( 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 ) ) ) ) }
 )   &    |-  ( ph  ->  ( X G Y )  e.  M )   &    |-  ( ph  ->  T  e.  ( S `  M ) )   &    |-  ( ph  ->  U  e.  II )   &    |-  ( ph  ->  V  e.  II )   &    |-  ( ph  ->  ( IIt  U )  e.  Con )   &    |-  ( ph  ->  ( IIt  V )  e.  Con )   &    |-  ( ph  ->  X  e.  U )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  ( U  X.  V ) 
 C_  ( `' G " M ) )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  ( K  |`  ( U  X.  { Z } ) )  e.  ( ( ( II  tX  II )t  ( U  X.  { Z }
 ) )  Cn  C ) )   &    |-  W  =  (
 iota_ b  e.  T ( X K Y )  e.  b )   =>    |-  ( ph  ->  ( K  |`  ( U  X.  V ) )  e.  ( ( ( II  tX  II )t  ( U  X.  V ) )  Cn  C ) )
 
Theoremcvmlift2lem10 23180* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   &    |-  S  =  ( 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 ) ) ) ) }
 )   &    |-  ( ph  ->  X  e.  ( 0 [,] 1
 ) )   &    |-  ( ph  ->  Y  e.  ( 0 [,] 1 ) )   =>    |-  ( ph  ->  E. u  e.  II  E. v  e.  II  ( X  e.  u  /\  Y  e.  v  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w }
 ) )  e.  (
 ( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  ->  ( K  |`  ( u  X.  v
 ) )  e.  (
 ( ( II  tX  II )t  ( u  X.  v
 ) )  Cn  C ) ) ) )
 
Theoremcvmlift2lem11 23181* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   &    |-  M  =  {
 z  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  |  K  e.  ( ( ( II  tX  II )  CnP  C ) `  z ) }   &    |-  ( ph  ->  U  e.  II )   &    |-  ( ph  ->  V  e.  II )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  Z  e.  V )   &    |-  ( ph  ->  ( E. w  e.  V  ( K  |`  ( U  X.  { w }
 ) )  e.  (
 ( ( II  tX  II )t  ( U  X.  { w } ) )  Cn  C )  ->  ( K  |`  ( U  X.  V ) )  e.  (
 ( ( II  tX  II )t  ( U  X.  V ) )  Cn  C ) ) )   =>    |-  ( ph  ->  (
 ( U  X.  { Y } )  C_  M  ->  ( U  X.  { Z } )  C_  M ) )
 
Theoremcvmlift2lem12 23182* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   &    |-  M  =  {
 z  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  |  K  e.  ( ( ( II  tX  II )  CnP  C ) `  z ) }   &    |-  A  =  { a  e.  (
 0 [,] 1 )  |  ( ( 0 [,] 1 )  X.  {
 a } )  C_  M }   &    |-  S  =  { <. r ,  t >.  |  ( t  e.  (
 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `  { r } )
 ( ( u  X.  { a } )  C_  M 
 <->  ( u  X.  {
 t } )  C_  M ) ) }   =>    |-  ( ph  ->  K  e.  (
 ( II  tX  II )  Cn  C ) )
 
Theoremcvmlift2lem13 23183* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   &    |-  H  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) ) 
 /\  ( f `  0 )  =  P ) )   &    |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 )  |->  ( ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  ( z  e.  ( 0 [,] 1 )  |->  ( x G z ) ) 
 /\  ( f `  0 )  =  ( H `  x ) ) ) `  y ) )   =>    |-  ( ph  ->  E! g  e.  ( ( II  tX  II )  Cn  C ) ( ( F  o.  g )  =  G  /\  (
 0 g 0 )  =  P ) )
 
Theoremcvmlift2 23184* A two-dimensional version of cvmlift 23167. There is a unique lift of functions on the unit square 
II  tX  II which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015.)
 |-  B  =  U. C   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  (
 0 G 0 ) )   =>    |-  ( ph  ->  E! f  e.  ( ( II  tX  II )  Cn  C ) ( ( F  o.  f )  =  G  /\  (
 0 f 0 )  =  P ) )
 
Theoremcvmliftphtlem 23185* Lemma for cvmliftpht 23186. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  M  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  0
 )  =  P ) )   &    |-  N  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  H  /\  ( f `  0
 )  =  P ) )   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0 ) )   &    |-  ( ph  ->  G  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  H  e.  ( II  Cn  J ) )   &    |-  ( ph  ->  K  e.  ( G ( PHtpy `  J ) H ) )   &    |-  ( ph  ->  A  e.  (
 ( II  tX  II )  Cn  C ) )   &    |-  ( ph  ->  ( F  o.  A )  =  K )   &    |-  ( ph  ->  (
 0 A 0 )  =  P )   =>    |-  ( ph  ->  A  e.  ( M (
 PHtpy `  C ) N ) )
 
Theoremcvmliftpht 23186* If  G and  H are path-homotopic, then their lifts  M and  N are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  M  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  0
 )  =  P ) )   &    |-  N  =  (
 iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f
 )  =  H  /\  ( f `  0
 )  =  P ) )   &    |-  ( ph  ->  F  e.  ( C CovMap  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  0 ) )   &    |-  ( ph  ->  G (  ~=ph  `  J ) H )   =>    |-  ( ph  ->  M (  ~=ph  `  C ) N )
 
Theoremcvmlift3lem1 23187* Lemma for cvmlift3 23196. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  ( ph  ->  M  e.  ( II  Cn  K ) )   &    |-  ( ph  ->  ( M `  0 )  =  O )   &    |-  ( ph  ->  N  e.  ( II  Cn  K ) )   &    |-  ( ph  ->  ( N `  0 )  =  O )   &    |-  ( ph  ->  ( M `  1 )  =  ( N `  1 ) )   =>    |-  ( ph  ->  ( ( iota_
 g  e.  ( II 
 Cn  C ) ( ( F  o.  g
 )  =  ( G  o.  M )  /\  ( g `  0
 )  =  P ) ) `  1 )  =  ( ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  N )  /\  ( g `
  0 )  =  P ) ) `  1 ) )
 
Theoremcvmlift3lem2 23188* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   =>    |-  ( ( ph  /\  X  e.  Y ) 
 ->  E! 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 ) )
 
Theoremcvmlift3lem3 23189* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   =>    |-  ( ph  ->  H : Y --> B )
 
Theoremcvmlift3lem4 23190* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   =>    |-  ( ( ph  /\  X  e.  Y )  ->  (
 ( H `  X )  =  A  <->  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
 )  =  A ) ) )
 
Theoremcvmlift3lem5 23191* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   =>    |-  ( ph  ->  ( F  o.  H )  =  G )
 
Theoremcvmlift3lem6 23192* Lemma for cvmlift3 23196. (Contributed by Mario Carneiro, 9-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   &    |-  S  =  ( 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 ) ) ) ) }
 )   &    |-  ( ph  ->  ( G `  X )  e.  A )   &    |-  ( ph  ->  T  e.  ( S `  A ) )   &    |-  ( ph  ->  M  C_  ( `' G " A ) )   &    |-  W  =  (
 iota_ b  e.  T ( H `  X )  e.  b )   &    |-  ( ph  ->  X  e.  M )   &    |-  ( ph  ->  Z  e.  M )   &    |-  ( ph  ->  Q  e.  ( II  Cn  K ) )   &    |-  R  =  ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g
 )  =  ( G  o.  Q )  /\  ( g `  0
 )  =  P ) )   &    |-  ( ph  ->  ( ( Q `  0
 )  =  O  /\  ( Q `  1 )  =  X  /\  ( R `  1 )  =  ( H `  X ) ) )   &    |-  ( ph  ->  N  e.  ( II  Cn  ( Kt  M ) ) )   &    |-  ( ph  ->  ( ( N `  0
 )  =  X  /\  ( N `  1 )  =  Z ) )   &    |-  I  =  ( iota_ g  e.  ( II  Cn  C ) ( ( F  o.  g )  =  ( G  o.  N )  /\  ( g `  0 )  =  ( H `  X ) ) )   =>    |-  ( ph  ->  ( H `  Z )  e.  W )
 
Theoremcvmlift3lem7 23193* Lemma for cvmlift3 23196. (Contributed by Mario Carneiro, 9-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   &    |-  S  =  ( 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 ) ) ) ) }
 )   &    |-  ( ph  ->  ( G `  X )  e.  A )   &    |-  ( ph  ->  T  e.  ( S `  A ) )   &    |-  ( ph  ->  M  C_  ( `' G " A ) )   &    |-  W  =  (
 iota_ b  e.  T ( H `  X )  e.  b )   &    |-  ( ph  ->  ( Kt  M )  e. PCon )   &    |-  ( ph  ->  V  e.  K )   &    |-  ( ph  ->  V  C_  M )   &    |-  ( ph  ->  X  e.  V )   =>    |-  ( ph  ->  H  e.  ( ( K  CnP  C ) `  X ) )
 
Theoremcvmlift3lem8 23194* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 6-Jul-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   &    |-  S  =  ( 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 ) ) ) ) }
 )   =>    |-  ( ph  ->  H  e.  ( K  Cn  C ) )
 
Theoremcvmlift3lem9 23195* Lemma for cvmlift2 23184. (Contributed by Mario Carneiro, 7-May-2015.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   &    |-  H  =  ( 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 ) ) )   &    |-  S  =  ( 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 ) ) ) ) }
 )   =>    |-  ( ph  ->  E. f  e.  ( K  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f `
  O )  =  P ) )
 
Theoremcvmlift3 23196* A general version of cvmlift 23167. 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.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e. SCon )   &    |-  ( ph  ->  K  e. 𝑛Locally PCon )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   =>    |-  ( ph  ->  E! f  e.  ( K  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  O )  =  P )
 )
 
16.4.10  Undirected multigraphs
 
Syntaxcumg 23197 Extend class notation with undirected multigraphs.
 class UMGrph
 
Syntaxceup 23198 Extend class notation with Eulerian paths.
 class EulPaths
 
Syntaxcvdg 23199 Extend class notation with the vertex degree function.
 class VDeg
 
Definitiondf-umgra 23200* Define the class of all undirected multigraphs. A multigraph is a pair  <. V ,  E >. where  E is a function into subsets of  V of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |- UMGrph  =  { <. v ,  e >.  |  e : dom  e --> { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x )  <_  2 } }
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-<