HomeHome Metamath Proof Explorer
Theorem List (p. 250 of 325)
< 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-22374)
  Hilbert Space Explorer  Hilbert Space Explorer
(22375-23897)
  Users' Mathboxes  Users' Mathboxes
(23898-32447)
 

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcvmtop2 24901 Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
 |-  ( F  e.  ( C CovMap  J )  ->  J  e.  Top )
 
Theoremcvmcn 24902 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 24903* 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 24904* 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 24905* One direction of cvmsval 24906. (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 24906* 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 24907* 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 24908* 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 24909* 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 24910* 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 24911* 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 24912*  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 24913* 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 24914* 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 24915* 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 24916* 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 24917* 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 24918* Lemma for cvmopn 24920. (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 24919* Lemma for cvmfo 24940. (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 24920 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 24921* Lemma for cvmliftmo 24924. (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 24922* Lemma for cvmliftmo 24924. (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 24923 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 24924* 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 24925* Lemma for cvmlift 24939. In cvmliftlem15 24938, 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 24926* Lemma for cvmlift 24939. 
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 24927* Lemma for cvmlift 24939. 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 24928* Lemma for cvmlift 24939. 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 24929* Lemma for cvmlift 24939. 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 24930* Lemma for cvmlift 24939. Induction step for cvmliftlem7 24931. 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 24931* Lemma for cvmlift 24939. Prove by induction that every  Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 24930 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 24932* Lemma for cvmlift 24939. 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 24933* Lemma for cvmlift 24939. 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 24934* Lemma for cvmlift 24939. 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 24930, cvmliftlem7 24931 (to show it is a function and a lift), cvmliftlem8 24932 (to show it is continuous), and cvmliftlem9 24933 (to show that different 
Q functions agree on the intersection of their domains, so that the pasting lemma paste 17312 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 24935* Lemma for cvmlift 24939. (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 24936* Lemma for cvmlift 24939. 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 24937* Lemma for cvmlift 24939. Putting the results of cvmliftlem11 24935, cvmliftlem13 24936 and cvmliftmo 24924 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 24938* Lemma for cvmlift 24939. Discharge the assumptions of cvmliftlem14 24937. 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 18944, 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 7310 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 24937. (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 24939* 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 24925 thru cvmliftlem15 24938. (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 24940 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 24941* 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 24942* Lemma for cvmlift2 24956. (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 24943* Lemma for cvmlift2 24956 and cvmlift3 24968. (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 24944* Lemma for cvmlift2 24956. (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 24945* Lemma for cvmlift2 24956. (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 24946* Lemma for cvmlift2 24956. (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 24947* Lemma for cvmlift2 24956. (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 24948* Lemma for cvmlift2 24956. (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 24949* Lemma for cvmlift2 24956. (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 24950* Lemma for cvmlift2 24956. (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 24951* Lemma for cvmlift2 24956. (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 24952* Lemma for cvmlift2 24956. (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 24953* Lemma for cvmlift2 24956. (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 24954* Lemma for cvmlift2 24956. (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 24955* Lemma for cvmlift2 24956. (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 24956* A two-dimensional version of cvmlift 24939. 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 24957* Lemma for cvmliftpht 24958. (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 24958* 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 24959* Lemma for cvmlift3 24968. (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 24960* Lemma for cvmlift2 24956. (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 24961* Lemma for cvmlift2 24956. (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 24962* Lemma for cvmlift2 24956. (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 24963* Lemma for cvmlift2 24956. (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 24964* Lemma for cvmlift3 24968. (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 24965* Lemma for cvmlift3 24968. (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 24966* Lemma for cvmlift2 24956. (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 24967* Lemma for cvmlift2 24956. (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 24968* A general version of cvmlift 24939. 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 )
 )
 
19.4.10  Normal numbers
 
Theoremsnmlff 24969* The function  F from snmlval 24971 is a mapping from positive integers to real numbers in the range 
[ 0 ,  1 ]. (Contributed by Mario Carneiro, 6-Apr-2015.)
 |-  F  =  ( n  e.  NN  |->  ( ( # `  { k  e.  ( 1 ... n )  |  ( |_ `  ( ( A  x.  ( R ^ k ) )  mod  R ) )  =  B }
 )  /  n )
 )   =>    |-  F : NN --> ( 0 [,] 1 )
 
Theoremsnmlfval 24970* The function  F from snmlval 24971 maps  N to the relative density of  B in the first  N digits of the digit string of  A in base  R. (Contributed by Mario Carneiro, 6-Apr-2015.)
 |-  F  =  ( n  e.  NN  |->  ( ( # `  { k  e.  ( 1 ... n )  |  ( |_ `  ( ( A  x.  ( R ^ k ) )  mod  R ) )  =  B }
 )  /  n )
 )   =>    |-  ( N  e.  NN  ->  ( F `  N )  =  ( ( # `
  { k  e.  ( 1 ... N )  |  ( |_ `  ( ( A  x.  ( R ^ k ) )  mod  R ) )  =  B }
 )  /  N )
 )
 
Theoremsnmlval 24971* The property " A is simply normal in base  R". A number is simply normal if each digit  0  <_  b  <  R occurs in the base-  R digit string of  A with frequency  1  /  R (which is consistent with the expectation in an infinite random string of numbers selected from  0 ... R  -  1). (Contributed by Mario Carneiro, 6-Apr-2015.)
 |-  S  =  ( r  e.  ( ZZ>=
 `  2 )  |->  { x  e.  RR  |  A. b  e.  (
 0 ... ( r  -  1 ) ) ( n  e.  NN  |->  ( ( # `  { k  e.  ( 1 ... n )  |  ( |_ `  ( ( x  x.  ( r ^ k
 ) )  mod  r
 ) )  =  b } )  /  n ) )  ~~>  ( 1  /  r ) } )   =>    |-  ( A  e.  ( S `  R )  <->  ( R  e.  ( ZZ>= `  2 )  /\  A  e.  RR  /\  A. b  e.  ( 0
 ... ( R  -  1 ) ) ( n  e.  NN  |->  ( ( # `  { k  e.  ( 1 ... n )  |  ( |_ `  ( ( A  x.  ( R ^ k ) )  mod  R ) )  =  b }
 )  /  n )
 )  ~~>  ( 1  /  R ) ) )
 
Theoremsnmlflim 24972* If  A is simply normal, then the function  F of relative density of  B in the digit string converges to  1  /  R, i.e. the set of occurences of  B in the digit string has natural density  1  /  R. (Contributed by Mario Carneiro, 6-Apr-2015.)
 |-  S  =  ( r  e.  ( ZZ>=
 `  2 )  |->  { x  e.  RR  |  A. b  e.  (
 0 ... ( r  -  1 ) ) ( n  e.  NN  |->  ( ( # `  { k  e.  ( 1 ... n )  |  ( |_ `  ( ( x  x.  ( r ^ k
 ) )  mod  r
 ) )  =  b } )  /  n ) )  ~~>  ( 1  /  r ) } )   &    |-  F  =  ( n  e.  NN  |->  ( ( # `  { k  e.  ( 1 ... n )  |  ( |_ `  ( ( A  x.  ( R ^ k ) )  mod  R ) )  =  B }
 )  /  n )
 )   =>    |-  ( ( A  e.  ( S `  R ) 
 /\  B  e.  (
 0 ... ( R  -  1 ) ) ) 
 ->  F  ~~>  ( 1  /  R ) )
 
19.4.11  Godel-sets of formulas
 
Syntaxcgoe 24973 The Godel-set of membership.
 class  e.g
 
Syntaxcgna 24974 The Godel-set for the Sheffer stroke.
 class  | g
 
Syntaxcgol 24975 The Godel-set of universal quantification. (Note that this is not a wff.)
 class  A.g N U
 
Syntaxcsat 24976 The satisfaction function.
 class  Sat
 
Syntaxcfmla 24977 The formula set predicate.
 class  Fmla
 
Syntaxcsate 24978 The  e.-satisfaction function.
 class  Sat E
 
Syntaxcprv 24979 The "proves" relation.
 class  |=
 
Definitiondf-goel 24980 Define the Godel-set of membership. Here the arguments  x  =  <. N ,  P >. correspond to vN and vP , so  ( (/)  e.g 
1o ) actually means v0  e. v1 , not  0  e.  1. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  e.g  =  ( x  e.  ( om  X.  om )  |->  <. (/)
 ,  x >. )
 
Definitiondf-gona 24981 Define the Godel-set for the Sheffer stroke NAND. Here the arguments  x  =  <. U ,  V >. are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  | g  =  ( x  e.  ( _V  X.  _V )  |->  <. 1o ,  x >. )
 
Definitiondf-goal 24982 Define the Godel-set of universal quantification. Here  N  e.  om corresponds to vN , and  U represents another formula, and this expression is  [ A. x ph ]  =  A.g N U where 
x is the  N-th variable,  U  =  [ ph ] is the code for  ph. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  A.g N U  =  <. 2o ,  <. N ,  U >. >.
 
Definitiondf-sat 24983* Define the satisfaction predicate. This recursive construction builds up a function over wff codes and simultaneously defines the set of assignments to all variables from  M that makes the coded wff true in the model  M, where  e. is interpreted as the binary relation  E on  M. The interpretation of the statement  S  e.  ( ( ( M  Sat  E ) `  n ) `  U ) is that for the model  <. M ,  E >.,  S : om --> M is a valuation of the variables (v0  =  ( S `  (/) ), v1  =  ( S `  1o ), etc.) and  U is a code for a wff using  =  ,  e.  ,  \/  ,  -.  ,  A. that is true under the assignment  S. The function is defined by finite recursion;  ( ( M  Sat  E ) `  n ) only operates on wffs of depth at most  n  e.  om, and  ( ( M  Sat  E ) `  om )  =  U_ n  e.  om ( ( M  Sat  E ) `  n ) operates on all wffs. The coding scheme for the wffs is defined so that
  • vi  e. vj is coded as  <. (/) ,  <. i ,  j >. >.,
  •  ( ph  -/\  ps ) is coded as  <. 1o ,  <. ph ,  ps >. >., and
  •  A. vi  ph is coded as  <. 2o ,  <. i ,  ph >. >..

(Contributed by Mario Carneiro, 14-Jul-2013.)

 |-  Sat  =  ( m  e.  _V ,  e  e.  _V  |->  ( rec ( ( f  e.  _V  |->  ( f  u.  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f  ( x  =  ( ( 1st `  u )  | g  ( 1st `  v
 ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
 ) ) ) )  \/  E. i  e. 
 om  ( x  = 
 A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  | 
 A. z  e.  m  ( { <. i ,  z >. }  u.  ( a  |`  ( om  \  {
 i } ) ) )  e.  ( 2nd `  u ) } )
 ) } ) ) ,  { <. x ,  y >.  |  E. i  e.  om  E. j  e. 
 om  ( x  =  ( i  e.g  j
 )  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i
 ) e ( a `
  j ) }
 ) } )  |`  suc  om ) )
 
Definitiondf-sate 24984* A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable  n. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  Sat E  =  ( m  e. 
 _V ,  u  e. 
 _V  |->  ( ( ( m  Sat  (  _E 
 i^i  ( m  X.  m ) ) ) `
  om ) `  u ) )
 
Definitiondf-fmla 24985 Define the predicate which defines the set of valid Godel formulas. The parameter  n defines the maximum height of the formulas: the set  ( Fmla `  (/) ) is all formulas of the form  x  =  y or  x  e.  y (which in our coding scheme is the set  ( { (/) ,  1o }  X.  ( om  X.  om ) ); see df-sat 24983 for the full coding scheme), and each extra level adds to the complexity of the formulas in  ( Fmla `  n
).  ( Fmla `  om )  =  U_ n  e. 
om ( Fmla `  n
) is the set of all valid formulas. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  Fmla  =  ( n  e.  suc  om 
 |->  dom  ( ( (/)  Sat  (/) ) `  n ) )
 
Syntaxcgon 24986 The Godel-set of negation. (Note that this is not a wff.)
 class  -.g U
 
Syntaxcgoa 24987 The Godel-set of conjunction.
 class  /\g
 
Syntaxcgoi 24988 The Godel-set of implication.
 class  ->g
 
Syntaxcgoo 24989 The Godel-set of disjunction.
 class  \/g
 
Syntaxcgob 24990 The Godel-set of equivalence.
 class  <->g
 
Syntaxcgoq 24991 The Godel-set of equality.
 class  =g
 
Syntaxcgox 24992 The Godel-set of existential quantification. (Note that this is not a wff.)
 class  E.g N U
 
Definitiondf-gonot 24993 Define the Godel-set of negation. Here the argument  U is also a Godel-set corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  -.g U  =  ( U  | g  U )
 
Definitiondf-goan 24994* Define the Godel-set of conjunction. Here the arguments  U and  V are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  /\g  =  ( u  e.  _V ,  v  e.  _V  |->  -.g ( u  | g  v ) )
 
Definitiondf-goim 24995* Define the Godel-set of implication. Here the arguments  U and  V are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  ->g  =  ( u  e.  _V ,  v  e.  _V  |->  ( u  | g  -.g v ) )
 
Definitiondf-goor 24996* Define the Godel-set of disjunction. Here the arguments  U and  V are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  \/g  =  ( u  e.  _V ,  v  e.  _V  |->  ( -.g u  ->g  v ) )
 
Definitiondf-gobi 24997* Define the Godel-set of equivalence. Here the arguments  U and  V are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  <->g  =  ( u  e.  _V ,  v  e.  _V  |->  ( ( u 
 ->g  v )  /\g  (
 v  ->g  u ) ) )
 
Definitiondf-goeq 24998* Define the Godel-set of equality. Here the arguments  x  =  <. N ,  P >. correspond to vN and vP , so  ( (/)  =g  1o ) actually means v0  = v1 , not  0  = 
1. Here we use the trick mentioned in ax-ext 2385 to introduce equality as a defined notion in terms of  e.g. The expression  suc  ( u  u.  v )  = max  ( u ,  v )  +  1 here is a convenient way of getting a dummy variable distinct from  u and  v. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  =g  =  ( u  e.  om ,  v  e.  om  |->  [_ suc  ( u  u.  v
 )  /  w ]_ A.g w ( ( w  e.g  u )  <->g  ( w  e.g  v
 ) ) )
 
Definitiondf-goex 24999 Define the Godel-set of existential quantification. Here  N  e.  om corresponds to vN , and  U represents another formula, and this expression is  [ E. x ph ]  =  E.g N U where 
x is the  N-th variable,  U  =  [ ph ] is the code for  ph. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  E.g N U  =  -.g A.g N -.g U
 
Definitiondf-prv 25000* Define the "proves" relation on a set. A wff is true in a model  M if for every valuation  s  e.  ( M  ^m  om ), the interpretation of the wff using the membership relation on  M is true. (Contributed by Mario Carneiro, 14-Jul-2013.)
 |-  |=  =  { <. m ,  u >.  |  ( m  Sat E  u )  =  ( m  ^m  om ) }
    < 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-