P. 313 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31201-31300   *Has distinct variable group(s)

Type	Label	Description
Statement
20.5.7  Path-connected and simply connected spaces
Syntax	cpconn 31201	Extend class notation with the class of path-connected topologies.
class PConn
Syntax	csconn 31202	Extend class notation with the class of simply connected topologies.
class SConn
Definition	df-pconn 31203*	Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the unit interval) that goes from x to y for any points x , y in the space. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- PConn = { j e. Top | A. x e. U. j A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) }
Definition	df-sconn 31204*	Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015.)
|- SConn = { j e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }
Theorem	ispconn 31205*	The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- X = U. J   =>    |- ( J e. PConn <-> ( J e. Top /\ A. x e. X A. y e. X E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
Theorem	pconncn 31206*	The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- X = U. J   =>    |- ( ( J e. PConn /\ A e. X /\ B e. X ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) )
Theorem	pconntop 31207	A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( J e. PConn -> J e. Top )
Theorem	issconn 31208*	The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( J e. SConn <-> ( J e. PConn /\ A. f e. ( II Cn J ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) ) )
Theorem	sconnpconn 31209	A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( J e. SConn -> J e. PConn )
Theorem	sconntop 31210	A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( J e. SConn -> J e. Top )
Theorem	sconnpht 31211	A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( J e. SConn /\ F e. ( II Cn J ) /\ ( F ` 0 ) = ( F ` 1 ) ) -> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
Theorem	cnpconn 31212	An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- Y = U. K   =>    |- ( ( J e. PConn /\ F : X -onto-> Y /\ F e. ( J Cn K ) ) -> K e. PConn )
Theorem	pconnconn 31213	A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( J e. PConn -> J e. Conn )
Theorem	txpconn 31214	The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- ( ( R e. PConn /\ S e. PConn ) -> ( R tX S ) e. PConn )
Theorem	ptpconn 31215	The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- ( ( A e. V /\ F : A -->PConn ) -> ( Xt_ ` F ) e. PConn )
Theorem	indispconn 31216	The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- { (/) , A } e. PConn
Theorem	connpconn 31217	A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.)
|- ( ( J e. Conn /\ J e. 𝑛Locally PConn ) -> J e. PConn )
Theorem	qtoppconn 31218	A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. PConn /\ F Fn X ) -> ( J qTop F ) e. PConn )
Theorem	pconnpi1 31219	All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- X = U. J   &    |- P = ( J pi1 A )   &    |- Q = ( J pi1 B )   &    |- S = ( Base ` P )   &    |- T = ( Base ` Q )   =>    |- ( ( J e. PConn /\ A e. X /\ B e. X ) -> P ~=g𝑔 Q )
Theorem	sconnpht2 31220	Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- ( ph -> J e. SConn )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- ( ph -> ( F ` 1 ) = ( G ` 1 ) )   =>    |- ( ph -> F ( ~=ph ` J ) G )
Theorem	sconnpi1 31221	A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- X = U. J   =>    |- ( ( J e. PConn /\ Y e. X ) -> ( J e. SConn <-> ( Base ` ( J pi1 Y ) ) ~~ 1o ) )
Theorem	txsconnlem 31222	Lemma for txsconn 31223. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- ( ph -> R e. Top )   &    |- ( ph -> S e. Top )   &    |- ( ph -> F e. ( II Cn ( R tX S ) ) )   &    |- A = ( ( 1st |` ( U. R X. U. S ) ) o. F )   &    |- B = ( ( 2nd |` ( U. R X. U. S ) ) o. F )   &    |- ( ph -> G e. ( A ( PHtpy ` R ) ( ( 0 [,] 1 ) X. { ( A ` 0 ) } ) ) )   &    |- ( ph -> H e. ( B ( PHtpy ` S ) ( ( 0 [,] 1 ) X. { ( B ` 0 ) } ) ) )   =>    |- ( ph -> F ( ~=ph ` ( R tX S ) ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
Theorem	txsconn 31223	The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- ( ( R e. SConn /\ S e. SConn ) -> ( R tX S ) e. SConn )
Theorem	cvxpconn 31224*	A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t S )   =>    |- ( ph -> K e. PConn )
Theorem	cvxsconn 31225*	A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t S )   =>    |- ( ph -> K e. SConn )
Theorem	blsconn 31226	An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- S = ( P ( ball ` ( abs o. - ) ) R )   &    |- K = ( J ↾t S )   =>    |- ( ( P e. CC /\ R e. RR* ) -> K e. SConn )
Theorem	cnllysconn 31227	The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Locally SConn
Theorem	resconn 31228	A subset of RR is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- J = ( ( topGen ` ran (,) ) ↾t A )   =>    |- ( A C_ RR -> ( J e. SConn <-> J e. Conn ) )
Theorem	ioosconn 31229	An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- ( ( topGen ` ran (,) ) ↾t ( A (,) B ) ) e. SConn
Theorem	iccsconn 31230	A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) e. SConn )
Theorem	retopsconn 31231	The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- ( topGen ` ran (,) ) e. SConn
Theorem	iccllysconn 31232	A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) e. Locally SConn )
Theorem	rellysconn 31233	The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( topGen ` ran (,) ) e. Locally SConn
Theorem	iisconn 31234	The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
|- II e. SConn
Theorem	iillysconn 31235	The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- II e. Locally SConn
Theorem	iinllyconn 31236	The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.)
|- II e. 𝑛Locally Conn
20.5.8  Covering maps
Syntax	ccvm 31237	Extend class notation with the class of covering maps.
class CovMap
Definition	df-cvm 31238*	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. ( ( c ↾t u ) Homeo ( j ↾t k ) ) ) ) ) } )
Theorem	fncvm 31239	Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
|- CovMap Fn ( Top X. Top )
Theorem	cvmscbv 31240*	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. ( ( C ↾t u ) Homeo ( J ↾t 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. ( ( C ↾t c ) Homeo ( J ↾t a ) ) ) ) } )
Theorem	iscvm 31241*	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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) =/= (/) ) ) )
Theorem	cvmtop1 31242	Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( F e. ( C CovMap J ) -> C e. Top )
Theorem	cvmtop2 31243	Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
|- ( F e. ( C CovMap J ) -> J e. Top )
Theorem	cvmcn 31244	A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.)
|- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
Theorem	cvmcov 31245*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   &    |- X = U. J   =>    |- ( ( F e. ( C CovMap J ) /\ P e. X ) -> E. x e. J ( P e. x /\ ( S ` x ) =/= (/) ) )
Theorem	cvmsrcl 31246*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( T e. ( S ` U ) -> U e. J )
Theorem	cvmsi 31247*	One direction of cvmsval 31248. (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. ( ( C ↾t u ) Homeo ( J ↾t 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. ( ( C ↾t u ) Homeo ( J ↾t U ) ) ) ) ) )
Theorem	cvmsval 31248*	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. ( ( C ↾t u ) Homeo ( J ↾t 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. ( ( C ↾t u ) Homeo ( J ↾t U ) ) ) ) ) ) )
Theorem	cvmsss 31249*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( T e. ( S ` U ) -> T C_ C )
Theorem	cvmsn0 31250*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( T e. ( S ` U ) -> T =/= (/) )
Theorem	cvmsuni 31251*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( T e. ( S ` U ) -> U. T = ( `' F " U ) )
Theorem	cvmsdisj 31252*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ( T e. ( S ` U ) /\ A e. T /\ B e. T ) -> ( A = B \/ ( A i^i B ) = (/) ) )
Theorem	cvmshmeo 31253*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ( T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) e. ( ( C ↾t A ) Homeo ( J ↾t U ) ) )
Theorem	cvmsf1o 31254*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) : A -1-1-onto-> U )
Theorem	cvmscld 31255*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. ( Clsd ` ( C ↾t ( `' F " U ) ) ) )
Theorem	cvmsss2 31256*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) -> ( ( S ` U ) =/= (/) -> ( S ` V ) =/= (/) ) )
Theorem	cvmcov2 31257*	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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> E. x e. ~P U ( P e. x /\ ( S ` x ) =/= (/) ) )
Theorem	cvmseu 31258*	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. ( ( C ↾t u ) Homeo ( J ↾t 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 )
Theorem	cvmsiota 31259*	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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) )
Theorem	cvmopnlem 31260*	Lemma for cvmopn 31262. (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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   &    |- B = U. C   =>    |- ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( F " A ) e. J )
Theorem	cvmfolem 31261*	Lemma for cvmfo 31282. (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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   &    |- B = U. C   &    |- X = U. J   =>    |- ( F e. ( C CovMap J ) -> F : B -onto-> X )
Theorem	cvmopn 31262	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 )
Theorem	cvmliftmolem1 31263*	Lemma for cvmliftmo 31266. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- B = U. C   &    |- Y = U. K   &    |- ( ph -> F e. ( C CovMap J ) )   &    |- ( ph -> K e. Conn )   &    |- ( ph -> K e. 𝑛Locally Conn )   &    |- ( 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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   &    |- ( ( ph /\ ps ) -> T e. ( S ` U ) )   &    |- ( ( ph /\ ps ) -> W e. T )   &    |- ( ( ph /\ ps ) -> I C_ ( `' M " W ) )   &    |- ( ( ph /\ ps ) -> ( K ↾t I ) e. Conn )   &    |- ( ( 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 ) ) )
Theorem	cvmliftmolem2 31264*	Lemma for cvmliftmo 31266. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- B = U. C   &    |- Y = U. K   &    |- ( ph -> F e. ( C CovMap J ) )   &    |- ( ph -> K e. Conn )   &    |- ( ph -> K e. 𝑛Locally Conn )   &    |- ( 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. ( ( C ↾t u ) Homeo ( J ↾t k ) ) ) ) } )   =>    |- ( ph -> M = N )
Theorem	cvmliftmoi 31265	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. Conn )   &    |- ( ph -> K e. 𝑛Locally Conn )   &    |- ( 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 )
Theorem	cvmliftmo 31266*	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. Conn )   &    |- ( ph -> K e. 𝑛Locally Conn )   &    |- ( 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 ) )
Theorem	cvmliftlem1 31267*	Lemma for cvmlift 31281. In cvmliftlem15 31280, 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) ) ) )
Theorem	cvmliftlem2 31268*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) )
Theorem	cvmliftlem3 31269*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) ) )
Theorem	cvmliftlem4 31270*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 >. }
Theorem	cvmliftlem5 31271*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) ) ) )
Theorem	cvmliftlem6 31272*	Lemma for cvmlift 31281. Induction step for cvmliftlem7 31273. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) ) )
Theorem	cvmliftlem7 31273*	Lemma for cvmlift 31281. Prove by induction that every Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 31272 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) ) } ) )
Theorem	cvmliftlem8 31274*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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. ( ( L ↾t W ) Cn C ) )
Theorem	cvmliftlem9 31275*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) ) )
Theorem	cvmliftlem10 31276*	Lemma for cvmlift 31281. 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 31272, cvmliftlem7 31273 (to show it is a function and a lift), cvmliftlem8 31274 (to show it is continuous), and cvmliftlem9 31275 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste 21098 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. ( ( C ↾t u ) Homeo ( J ↾t 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. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )   =>    |- ( ph -> ( K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )
Theorem	cvmliftlem11 31277*	Lemma for cvmlift 31281. (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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) )
Theorem	cvmliftlem13 31278*	Lemma for cvmlift 31281. 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. ( ( C ↾t u ) Homeo ( J ↾t 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 )
Theorem	cvmliftlem14 31279*	Lemma for cvmlift 31281. Putting the results of cvmliftlem11 31277, cvmliftlem13 31278 and cvmliftmo 31266 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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) )
Theorem	cvmliftlem15 31280*	Lemma for cvmlift 31281. Discharge the assumptions of cvmliftlem14 31279. 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 22765, 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 8204 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 31279. (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. ( ( C ↾t u ) Homeo ( J ↾t 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 ) )
Theorem	cvmlift 31281*	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 31267 thru cvmliftlem15 31280. (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 ) )
Theorem	cvmfo 31282	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 )
Theorem	cvmliftiota 31283*	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 ) )
Theorem	cvmlift2lem1 31284*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem9a 31285*	Lemma for cvmlift2 31298 and cvmlift3 31310. (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. ( ( C ↾t c ) Homeo ( J ↾t 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. ( ( K ↾t M ) Cn C ) )
Theorem	cvmlift2lem2 31286*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem3 31287*	Lemma for cvmlift2 31298. (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 ) ) )
Theorem	cvmlift2lem4 31288*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem5 31289*	Lemma for cvmlift2 31298. (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 )
Theorem	cvmlift2lem6 31290*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem7 31291*	Lemma for cvmlift2 31298. (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 )
Theorem	cvmlift2lem8 31292*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem9 31293*	Lemma for cvmlift2 31298. (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. ( ( C ↾t c ) Homeo ( J ↾t k ) ) ) ) } )   &    |- ( ph -> ( X G Y ) e. M )   &    |- ( ph -> T e. ( S ` M ) )   &    |- ( ph -> U e. II )   &    |- ( ph -> V e. II )   &    |- ( ph -> ( II ↾t U ) e. Conn )   &    |- ( ph -> ( II ↾t V ) e. Conn )   &    |- ( 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 ) )
Theorem	cvmlift2lem10 31294*	Lemma for cvmlift2 31298. (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. ( ( C ↾t c ) Homeo ( J ↾t 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 ) ) ) )
Theorem	cvmlift2lem11 31295*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem12 31296*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2lem13 31297*	Lemma for cvmlift2 31298. (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 ) )
Theorem	cvmlift2 31298*	A two-dimensional version of cvmlift 31281. 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 ) )
Theorem	cvmliftphtlem 31299*	Lemma for cvmliftpht 31300. (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 ) )
Theorem	cvmliftpht 31300*	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 )