HomeHome Metamath Proof Explorer
Theorem List (p. 239 of 328)
< 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-21514)
  Hilbert Space Explorer  Hilbert Space Explorer
(21515-23037)
  Users' Mathboxes  Users' Mathboxes
(23038-32776)
 

Theorem List for Metamath Proof Explorer - 23801-23900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
18.4.9  Covering maps
 
Syntaxccvm 23801 Extend class notation with the class of covering maps.
 class CovMap
 
Definitiondf-cvm 23802* 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 23803 Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |- CovMap  Fn  ( Top  X.  Top )
 
Theoremcvmscbv 23804* 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 23805* 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 23806 Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
 |-  ( F  e.  ( C CovMap  J )  ->  C  e.  Top )
 
Theoremcvmtop2 23807 Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  ( F  e.  ( C CovMap  J )  ->  J  e.  Top )
 
Theoremcvmcn 23808 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 23809* 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 23810* 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 23811* One direction of cvmsval 23812. (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 23812* 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 23813* 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 23814* 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 23815* 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 23816* 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 23817* 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 23818*  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 23819* 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 23820* 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 23821* 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 23822* 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 23823* 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 23824* Lemma for cvmopn 23826. (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 23825* Lemma for cvmfo 23846. (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 23826 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 23827* Lemma for cvmliftmo 23830. (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 23828* Lemma for cvmliftmo 23830. (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 23829 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 23830* 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.) (Revised by NM, 17-Jun-2017.)
 |-  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  e.  ( K  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  O )  =  P )
 )
 
Theoremcvmliftlem1 23831* Lemma for cvmlift 23845. In cvmliftlem15 23844, 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 23832* Lemma for cvmlift 23845. 
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 23833* Lemma for cvmlift 23845. 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 23834* Lemma for cvmlift 23845. 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 23835* Lemma for cvmlift 23845. 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 23836* Lemma for cvmlift 23845. Induction step for cvmliftlem7 23837. 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 23837* Lemma for cvmlift 23845. Prove by induction that every  Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 23836 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 23838* Lemma for cvmlift 23845. 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 23839* Lemma for cvmlift 23845. 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 23840* Lemma for cvmlift 23845. 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 23836, cvmliftlem7 23837 (to show it is a function and a lift), cvmliftlem8 23838 (to show it is continuous), and cvmliftlem9 23839 (to show that different 
Q functions agree on the intersection of their domains, so that the pasting lemma paste 17038 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 23841* Lemma for cvmlift 23845. (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 23842* Lemma for cvmlift 23845. 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 23843* Lemma for cvmlift 23845. Putting the results of cvmliftlem11 23841, cvmliftlem13 23842 and cvmliftmo 23830 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 23844* Lemma for cvmlift 23845. Discharge the assumptions of cvmliftlem14 23843. 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 18480, 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 7117 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 23843. (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 23845* 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 23831 thru cvmliftlem15 23844. (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 23846 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 23847* 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 23848* Lemma for cvmlift2 23862. (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 23849* Lemma for cvmlift2 23862 and cvmlift3 23874. (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 23850* Lemma for cvmlift2 23862. (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 23851* Lemma for cvmlift2 23862. (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 23852* Lemma for cvmlift2 23862. (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 23853* Lemma for cvmlift2 23862. (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 23854* Lemma for cvmlift2 23862. (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 23855* Lemma for cvmlift2 23862. (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 23856* Lemma for cvmlift2 23862. (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 23857* Lemma for cvmlift2 23862. (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 23858* Lemma for cvmlift2 23862. (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 23859* Lemma for cvmlift2 23862. (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 23860* Lemma for cvmlift2 23862. (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 23861* Lemma for cvmlift2 23862. (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 23862* A two-dimensional version of cvmlift 23845. 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 23863* Lemma for cvmliftpht 23864. (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 23864* 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 23865* Lemma for cvmlift3 23874. (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 23866* Lemma for cvmlift2 23862. (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 23867* Lemma for cvmlift2 23862. (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 23868* Lemma for cvmlift2 23862. (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 23869* Lemma for cvmlift2 23862. (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 23870* Lemma for cvmlift3 23874. (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 23871* Lemma for cvmlift3 23874. (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 23872* Lemma for cvmlift2 23862. (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 23873* Lemma for cvmlift2 23862. (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 23874* A general version of cvmlift 23845. 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 )
 )
 
18.4.10  Undirected multigraphs
 
Syntaxcumg 23875 Extend class notation with undirected multigraphs.
 class UMGrph
 
Syntaxceup 23876 Extend class notation with Eulerian paths.
 class EulPaths
 
Syntaxcvdg 23877 Extend class notation with the vertex degree function.
 class VDeg
 
Definitiondf-umgra 23878* 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 } }
 
Definitiondf-eupa 23879* Define the set of all Eulerian paths on an undirected multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |- EulPaths  =  ( v  e.  _V ,  e  e.  _V  |->  { <. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1
 ... n ) ( e `  ( f `
  k ) )  =  { ( p `
  ( k  -  1 ) ) ,  ( p `  k
 ) } ) ) } )
 
Definitiondf-vdgr 23880* Define the vertex degree function for an undirected multigraph. We have to double-count those edges that contain  u "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |- VDeg  =  ( v  e.  _V ,  e  e.  _V  |->  ( u  e.  v  |->  ( ( # `  { x  e. 
 dom  e  |  u  e.  ( e `  x ) } )  +  ( # `
  { x  e. 
 dom  e  |  ( e `  x )  =  { u } } ) ) ) )
 
Theoremrelumgra 23881 The class of all undirected multigraphs is a relation. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  Rel UMGrph
 
Theoremisumgra 23882* The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V  e.  W  /\  E  e.  X ) 
 ->  ( V UMGrph  E  <->  E : dom  E --> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  <_  2 } )
 )
 
Theoremwrdumgra 23883* The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V  e.  W  /\  E  e. Word  X )  ->  ( V UMGrph  E  <->  E  e. Word  { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  <_  2 } )
 )
 
Theoremumgraf2 23884* The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  ( V UMGrph  E  ->  E : dom  E --> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  <_  2 } )
 
Theoremumgraf 23885* The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V UMGrph  E  /\  E  Fn  A )  ->  E : A --> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  <_  2 } )
 
Theoremumgrass 23886 An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V UMGrph  E  /\  E  Fn  A  /\  F  e.  A )  ->  ( E `  F )  C_  V )
 
Theoremumgran0 23887 An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V UMGrph  E  /\  E  Fn  A  /\  F  e.  A )  ->  ( E `  F )  =/=  (/) )
 
Theoremumgrale 23888 An edge has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V UMGrph  E  /\  E  Fn  A  /\  F  e.  A )  ->  ( # `
  ( E `  F ) )  <_ 
 2 )
 
Theoremumgrafi 23889 An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V UMGrph  E  /\  E  Fn  A  /\  F  e.  A )  ->  ( E `  F )  e. 
 Fin )
 
Theoremumgraex 23890* An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
 |-  (
 ( V UMGrph  E  /\  E  Fn  A  /\  F  e.  A )  ->  E. x  e.  V  E. y  e.  V  ( E `  F )  =  { x ,  y }
 )
 
Theoremumgrares 23891 A subgraph of a graph (formed by removing some edges from the original graph) is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  ( V UMGrph  E  ->  V UMGrph  ( E  |`  A ) )
 
Theoremumgra0 23892 The empty graph, with vertices but no edges, is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  ( V  e.  W  ->  V UMGrph  (/) )
 
Theoremumgra1 23893 The graph with one edge. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  (
 ( ( V  e.  W  /\  A  e.  X )  /\  ( B  e.  V  /\  C  e.  V ) )  ->  V UMGrph  { <. A ,  { B ,  C } >. } )
 
Theoremumgraun 23894 If  <. V ,  E >. and  <. V ,  F >. are graphs, then  <. V ,  E  u.  F >. is a graph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  ( ph  ->  E  Fn  A )   &    |-  ( ph  ->  F  Fn  B )   &    |-  ( ph  ->  ( A  i^i  B )  =  (/) )   &    |-  ( ph  ->  V UMGrph  E )   &    |-  ( ph  ->  V UMGrph  F )   =>    |-  ( ph  ->  V UMGrph  ( E  u.  F ) )
 
Theoremreleupa 23895 The set  ( V EulPaths  E ) of all Eulerian paths on  <. V ,  E >. is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  Rel  ( V EulPaths  E )
 
Theoremiseupa 23896* The property " <. F ,  P >. is an Eulerian path on the graph  <. V ,  E >.". An Eulerian path is defined as bijection  F from the edges to a set  1 ... N a function  P :
( 0 ... N
) --> V into the vertices such that for each 
1  <_  k  <_  N,  F ( k ) is an edge from  P ( k  -  1 ) to  P
( k ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)
 |-  ( dom  E  =  A  ->  ( F ( V EulPaths  E ) P  <->  ( V UMGrph  E  /\  E. n  e.  NN0  ( F : ( 1
 ... n ) -1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1
 ... n ) ( E `  ( F `
  k ) )  =  { ( P `
  ( k  -  1 ) ) ,  ( P `  k
 ) } ) ) ) )
 
Theoremeupagra 23897 If an eulerian path exists, then 
<. V ,  E >. is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  ( F ( V EulPaths  E ) P  ->  V UMGrph  E )
 
Theoremeupai 23898* Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  (
 ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  ( ( ( # `  F )  e.  NN0  /\  F : ( 1
 ... ( # `  F ) ) -1-1-onto-> A  /\  P :
 ( 0 ... ( # `
  F ) ) --> V )  /\  A. k  e.  ( 1 ... ( # `  F ) ) ( E `
  ( F `  k ) )  =  { ( P `  ( k  -  1
 ) ) ,  ( P `  k ) }
 ) )
 
Theoremeupacl 23899 An Eulerian path has length 
# ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  ( F ( V EulPaths  E ) P  ->  ( # `  F )  e.  NN0 )
 
Theoremeupaf1o 23900 The  F function in an Eulerian path is a bijection from a one-based sequence to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.)
 |-  (
 ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  F : ( 1 ... ( # `  F ) ) -1-1-onto-> A )
    < 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