P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	kur14lem9 35801*	Lemma for kur14 35803. Since the set 𝑇 is closed under closure and complement, it contains the minimal set 𝑆 as a subset, so 𝑆 also has at most 14 elements. (Indeed 𝑆 = 𝑇, and it's not hard to prove this, but we don't need it for this proof.) (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    &   ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴))    &   ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴))    &   ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴))    &   ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))}))    &   ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)}    ⇒   ⊢ (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14)
Theorem	kur14lem10 35802*	Lemma for kur14 35803. Discharge the set 𝑇. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)}    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14)
Theorem	kur14 35803*	Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)}    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14))
21.6.6  Retracts and sections
Syntax	cretr 35804	Extend class notation with the retract relation.
class Retr
Definition	df-retr 35805*	Define the set of retractions on two topological spaces. We say that 𝑅 is a retraction from 𝐽 to 𝐾. or 𝑅 ∈ (𝐽 Retr 𝐾) iff there is an 𝑆 such that 𝑅:𝐽⟶𝐾, 𝑆:𝐾⟶𝐽 are continuous functions called the retraction and section respectively, and their composite 𝑅 ∘ 𝑆 is homotopic to the identity map. If a retraction exists, we say 𝐽 is a retract of 𝐾. (This terminology is borrowed from HoTT and appears to be nonstandard, although it has similaries to the concept of retract in the category of topological spaces and to a deformation retract in general topology.) Two topological spaces that are retracts of each other are called homotopy equivalent. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ Retr = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅})
21.6.7  Path-connected and simply connected spaces
Syntax	cpconn 35806	Extend class notation with the class of path-connected topologies.
class PConn
Syntax	csconn 35807	Extend class notation with the class of simply connected topologies.
class SConn
Definition	df-pconn 35808*	Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the closed unit interval) that goes from 𝑥 to 𝑦 for any points 𝑥, 𝑦 in the space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
Definition	df-sconn 35809*	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 = {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}
Theorem	ispconn 35810*	The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
Theorem	pconncn 35811*	The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐵))
Theorem	pconntop 35812	A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ PConn → 𝐽 ∈ Top)
Theorem	issconn 35813*	The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ SConn ↔ (𝐽 ∈ PConn ∧ ∀𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝐽)((0[,]1) × {(𝑓‘0)}))))
Theorem	sconnpconn 35814	A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ SConn → 𝐽 ∈ PConn)
Theorem	sconntop 35815	A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ SConn → 𝐽 ∈ Top)
Theorem	sconnpht 35816	A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝐽 ∈ SConn ∧ 𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = (𝐹‘1)) → 𝐹( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)}))
Theorem	cnpconn 35817	An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ PConn)
Theorem	pconnconn 35818	A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ PConn → 𝐽 ∈ Conn)
Theorem	txpconn 35819	The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ ((𝑅 ∈ PConn ∧ 𝑆 ∈ PConn) → (𝑅 ×t 𝑆) ∈ PConn)
Theorem	ptpconn 35820	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) → (∏t‘𝐹) ∈ PConn)
Theorem	indispconn 35821	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.)
⊢ {∅, 𝐴} ∈ PConn
Theorem	connpconn 35822	A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn) → 𝐽 ∈ PConn)
Theorem	qtoppconn 35823	A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ PConn)
Theorem	pconnpi1 35824	All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑃 = (𝐽 π1 𝐴)    &   ⊢ 𝑄 = (𝐽 π1 𝐵)    &   ⊢ 𝑆 = (Base‘𝑃)    &   ⊢ 𝑇 = (Base‘𝑄)    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑃 ≃𝑔 𝑄)
Theorem	sconnpht2 35825	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.)
⊢ (𝜑 → 𝐽 ∈ SConn)    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘1))    ⇒   ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺)
Theorem	sconnpi1 35826	A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋) → (𝐽 ∈ SConn ↔ (Base‘(𝐽 π1 𝑌)) ≈ 1o))
Theorem	txsconnlem 35827	Lemma for txsconn 35828. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ (𝜑 → 𝑅 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ∈ Top)    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn (𝑅 ×t 𝑆)))    &   ⊢ 𝐴 = ((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝐹)    &   ⊢ 𝐵 = ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐴(PHtpy‘𝑅)((0[,]1) × {(𝐴‘0)})))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐵(PHtpy‘𝑆)((0[,]1) × {(𝐵‘0)})))    ⇒   ⊢ (𝜑 → 𝐹( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝐹‘0)}))
Theorem	txsconn 35828	The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn)
Theorem	cvxpconn 35829*	A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11208. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ (𝜑 → 𝐾 ∈ PConn)
Theorem	cvxsconn 35830*	A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11208. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ (𝜑 → 𝐾 ∈ SConn)
Theorem	blsconn 35831	An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ ((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → 𝐾 ∈ SConn)
Theorem	cnllysconn 35832	The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Locally SConn
Theorem	resconn 35833	A subset of ℝ is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ SConn ↔ 𝐽 ∈ Conn))
Theorem	ioosconn 35834	An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((topGen‘ran (,)) ↾t (𝐴(,)𝐵)) ∈ SConn
Theorem	iccsconn 35835	A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ SConn)
Theorem	retopsconn 35836	The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ SConn
Theorem	iccllysconn 35837	A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn)
Theorem	rellysconn 35838	The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ Locally SConn
Theorem	iisconn 35839	The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ II ∈ SConn
Theorem	iillysconn 35840	The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ II ∈ Locally SConn
Theorem	iinllyconn 35841	The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ II ∈ 𝑛-Locally Conn
21.6.8  Covering maps
Syntax	ccvm 35842	Extend class notation with the class of covering maps.
class CovMap
Definition	df-cvm 35843*	Define the class of covering maps on two topological spaces. A function 𝑓:𝑐⟶𝑗 is a covering map if it is continuous and for every point 𝑥 in the target space there is a neighborhood 𝑘 of 𝑥 and a decomposition 𝑠 of the preimage of 𝑘 as a disjoint union such that 𝑓 is a homeomorphism of each set 𝑢 ∈ 𝑠 onto 𝑘. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))})
Theorem	fncvm 35844	Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ CovMap Fn (Top × Top)
Theorem	cvmscbv 35845*	Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (◡𝐹 “ 𝑎) ∧ ∀𝑐 ∈ 𝑏 (∀𝑑 ∈ (𝑏 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑎))))})
Theorem	iscvm 35846*	The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) ↔ ((𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ (𝐶 Cn 𝐽)) ∧ ∀𝑥 ∈ 𝑋 ∃𝑘 ∈ 𝐽 (𝑥 ∈ 𝑘 ∧ (𝑆‘𝑘) ≠ ∅)))
Theorem	cvmtop1 35847	Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
Theorem	cvmtop2 35848	Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
Theorem	cvmcn 35849	A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
Theorem	cvmcov 35850*	Property of a covering map. In order to make the covering property more manageable, we define here the set 𝑆(𝑘) of all even coverings of an open set 𝑘 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.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑃 ∈ 𝑋) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅))
Theorem	cvmsrcl 35851*	Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽)
Theorem	cvmsi 35852*	One direction of cvmsval 35853. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈))))))
Theorem	cvmsval 35853*	Elementhood in the set 𝑆 of all even coverings of an open set in 𝐽. 𝑆 is an even covering of 𝑈 if it is a nonempty collection of disjoint open sets in 𝐶 whose union is the preimage of 𝑈, such that each set 𝑢 ∈ 𝑆 is homeomorphic under 𝐹 to 𝑈. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝑇 ∈ (𝑆‘𝑈) ↔ (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈)))))))
Theorem	cvmsss 35854*	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.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
Theorem	cvmsn0 35855*	An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅)
Theorem	cvmsuni 35856*	An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
Theorem	cvmsdisj 35857*	An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	cvmshmeo 35858*	Every element of an even covering of 𝑈 is homeomorphic to 𝑈 via 𝐹. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → (𝐹 ↾ 𝐴) ∈ ((𝐶 ↾t 𝐴)Homeo(𝐽 ↾t 𝑈)))
Theorem	cvmsf1o 35859*	𝐹, localized to an element of an even covering of 𝑈, is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → (𝐹 ↾ 𝐴):𝐴–1-1-onto→𝑈)
Theorem	cvmscld 35860*	The sets of an even covering are clopen in the subspace topology on 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → 𝐴 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
Theorem	cvmsss2 35861*	An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅))
Theorem	cvmcov2 35862*	The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑥 ∈ 𝒫 𝑈(𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅))
Theorem	cvmseu 35863*	Every element in ∪ 𝑇 is a member of a unique element of 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥)
Theorem	cvmsiota 35864*	Identify the unique element of 𝑇 containing 𝐴. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑊 = (℩𝑥 ∈ 𝑇 𝐴 ∈ 𝑥)    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊))
Theorem	cvmopnlem 35865*	Lemma for cvmopn 35867. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cvmfolem 35866*	Lemma for cvmfo 35887. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋)
Theorem	cvmopn 35867	A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cvmliftmolem1 35868*	Lemma for cvmliftmo 35871. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))
Theorem	cvmliftmolem2 35869*	Lemma for cvmliftmo 35871. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	cvmliftmoi 35870	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.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	cvmliftmo 35871*	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.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    ⇒   ⊢ (𝜑 → ∃*𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃))
Theorem	cvmliftlem1 35872*	Lemma for cvmlift 35886. In cvmliftlem15 35885, we picked an 𝑁 large enough so that the sections (𝐺 “ [(𝑘 − 1) / 𝑁, 𝑘 / 𝑁]) are all contained in an even covering, and the function 𝑇 enumerates these even coverings. So 1st ‘(𝑇‘𝑀) is a neighborhood of (𝐺 “ [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁]), and 2nd ‘(𝑇‘𝑀) is an even covering of 1st ‘(𝑇‘𝑀), which is to say a disjoint union of open sets in 𝐶 whose image is 1st ‘(𝑇‘𝑀). (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (2nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1st ‘(𝑇‘𝑀))))
Theorem	cvmliftlem2 35873*	Lemma for cvmlift 35886. 𝑊 = [(𝑘 − 1) / 𝑁, 𝑘 / 𝑁] is a subset of [0, 1] for each 𝑀 ∈ (1...𝑁). (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))    &   ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (0[,]1))
Theorem	cvmliftlem3 35874*	Lemma for cvmlift 35886. Since 1st ‘(𝑇‘𝑀) is a neighborhood of (𝐺 “ 𝑊), every element 𝐴 ∈ 𝑊 satisfies (𝐺‘𝐴) ∈ (1st ‘(𝑇‘𝑀)). (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))    &   ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐴) ∈ (1st ‘(𝑇‘𝑀)))
Theorem	cvmliftlem4 35875*	Lemma for cvmlift 35886. The function 𝑄 will be our lifted path, defined piecewise on each section [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] for 𝑀 ∈ (1...𝑁). For 𝑀 = 0, it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to 𝑃. (Contributed by Mario Carneiro, 15-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    ⇒   ⊢ (𝑄‘0) = {⟨0, 𝑃⟩}
Theorem	cvmliftlem5 35876*	Lemma for cvmlift 35886. Definition of 𝑄 at a successor. This is a function defined on 𝑊 as ◡(𝑇 ↾ 𝐼) ∘ 𝐺 where 𝐼 is the unique covering set of 2nd ‘(𝑇‘𝑀) that contains 𝑄(𝑀 − 1) evaluated at the last defined point, namely (𝑀 − 1) / 𝑁 (note that for 𝑀 = 1 this is using the seed value 𝑄(0)(0) = 𝑃). (Contributed by Mario Carneiro, 15-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))
Theorem	cvmliftlem6 35877*	Lemma for cvmlift 35886. Induction step for cvmliftlem7 35878. Assuming that 𝑄(𝑀 − 1) is defined at (𝑀 − 1) / 𝑁 and is a preimage of 𝐺((𝑀 − 1) / 𝑁), the next segment 𝑄(𝑀) is also defined and is a function on 𝑊 which is a lift 𝐺 for this segment. This follows explicitly from the definition 𝑄(𝑀) = ◡(𝐹 ↾ 𝐼) ∘ 𝐺 since 𝐺 is in 1st ‘(𝐹‘𝑀) for the entire interval so that ◡(𝐹 ↾ 𝐼) maps this into 𝐼 and 𝐹 ∘ 𝑄 maps back to 𝐺. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘𝑀):𝑊⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑀)) = (𝐺 ↾ 𝑊)))
Theorem	cvmliftlem7 35878*	Lemma for cvmlift 35886. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 35877 to show functionality and lifting of 𝑄). (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
Theorem	cvmliftlem8 35879*	Lemma for cvmlift 35886. The functions 𝑄 are continuous functions because they are defined as ◡(𝐹 ↾ 𝐼) ∘ 𝐺 where 𝐺 is continuous and (𝐹 ↾ 𝐼) is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑄‘𝑀) ∈ ((𝐿 ↾t 𝑊) Cn 𝐶))
Theorem	cvmliftlem9 35880*	Lemma for cvmlift 35886. The 𝑄(𝑀) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the 𝑄 functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘𝑀)‘((𝑀 − 1) / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)))
Theorem	cvmliftlem10 35881*	Lemma for cvmlift 35886. The function 𝐾 is going to be our complete lifted path, formed by unioning together all the 𝑄 functions (each of which is defined on one segment [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] of the interval). Here we prove by induction that 𝐾 is a continuous function and a lift of 𝐺 by applying cvmliftlem6 35877, cvmliftlem7 35878 (to show it is a function and a lift), cvmliftlem8 35879 (to show it is continuous), and cvmliftlem9 35880 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23525 gives that 𝐾 is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)    &   ⊢ (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))    ⇒   ⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
Theorem	cvmliftlem11 35882*	Lemma for cvmlift 35886. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)    ⇒   ⊢ (𝜑 → (𝐾 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = 𝐺))
Theorem	cvmliftlem13 35883*	Lemma for cvmlift 35886. The initial value of 𝐾 is 𝑃 because 𝑄(1) is a subset of 𝐾 which takes value 𝑃 at 0. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)    ⇒   ⊢ (𝜑 → (𝐾‘0) = 𝑃)
Theorem	cvmliftlem14 35884*	Lemma for cvmlift 35886. Putting the results of cvmliftlem11 35882, cvmliftlem13 35883 and cvmliftmo 35871 together, we have that 𝐾 is a continuous function, satisfies 𝐹 ∘ 𝐾 = 𝐺 and 𝐾(0) = 𝑃, and is equal to any other function which also has these properties, so it follows that 𝐾 is the unique lift of 𝐺. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘)))    &   ⊢ 𝐿 = (topGen‘ran (,))    &   ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))    &   ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmliftlem15 35885*	Lemma for cvmlift 35886. Discharge the assumptions of cvmliftlem14 35884. The set of all open subsets 𝑢 of the unit interval such that 𝐺 “ 𝑢 is contained in an even covering of some open set in 𝐽 is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii 25200, there is a subdivision of the closed unit interval into 𝑁 equal parts such that each part is entirely contained within one such open set of 𝐽. Then using finite choice ac6sfi 9258 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 35884. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmlift 35886*	One of the important properties of covering maps is that any path 𝐺 in the base space "lifts" to a path 𝑓 in the covering space such that 𝐹 ∘ 𝑓 = 𝐺, and given a starting point 𝑃 in the covering space this lift is unique. The proof is contained in cvmliftlem1 35872 thru cvmliftlem15 35885. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmfo 35887	A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋)
Theorem	cvmliftiota 35888*	Write out a function 𝐻 that is the unique lift of 𝐹. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    ⇒   ⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = 𝐺 ∧ (𝐻‘0) = 𝑃))
Theorem	cvmlift2lem1 35889*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ (∀𝑦 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
Theorem	cvmlift2lem9a 35890*	Lemma for cvmlift2 35903 and cvmlift3 35915. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐻:𝑌⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))    &   ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝑌)    &   ⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊)    ⇒   ⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶))
Theorem	cvmlift2lem2 35891*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    ⇒   ⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
Theorem	cvmlift2lem3 35892*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝐾‘0) = (𝐻‘𝑋)))
Theorem	cvmlift2lem4 35893*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    ⇒   ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝑋𝐾𝑌) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑌))
Theorem	cvmlift2lem5 35894*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    ⇒   ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
Theorem	cvmlift2lem6 35895*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶))
Theorem	cvmlift2lem7 35896*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺)
Theorem	cvmlift2lem8 35897*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑋𝐾0) = (𝐻‘𝑋))
Theorem	cvmlift2lem9 35898*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝑀))    &   ⊢ (𝜑 → 𝑈 ∈ II)    &   ⊢ (𝜑 → 𝑉 ∈ II)    &   ⊢ (𝜑 → (II ↾t 𝑈) ∈ Conn)    &   ⊢ (𝜑 → (II ↾t 𝑉) ∈ Conn)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (◡𝐺 “ 𝑀))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn 𝐶))    &   ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝑋𝐾𝑌) ∈ 𝑏)    ⇒   ⊢ (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II) ↾t (𝑈 × 𝑉)) Cn 𝐶))
Theorem	cvmlift2lem10 35899*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → 𝑋 ∈ (0[,]1))    &   ⊢ (𝜑 → 𝑌 ∈ (0[,]1))    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))))
Theorem	cvmlift2lem11 35900*	Lemma for cvmlift2 35903. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    &   ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))    &   ⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧)}    &   ⊢ (𝜑 → 𝑈 ∈ II)    &   ⊢ (𝜑 → 𝑉 ∈ II)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → (∃𝑤 ∈ 𝑉 (𝐾 ↾ (𝑈 × {𝑤})) ∈ (((II ×t II) ↾t (𝑈 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II) ↾t (𝑈 × 𝑉)) Cn 𝐶)))    ⇒   ⊢ (𝜑 → ((𝑈 × {𝑌}) ⊆ 𝑀 → (𝑈 × {𝑍}) ⊆ 𝑀))