P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qtoppconn 36001	A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ PConn)
Theorem	pconnpi1 36002	All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑃 = (𝐽 π1 𝐴)    &   ⊢ 𝑄 = (𝐽 π1 𝐵)    &   ⊢ 𝑆 = (Base‘𝑃)    &   ⊢ 𝑇 = (Base‘𝑄)    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑃 ≃𝑔 𝑄)
Theorem	sconnpht2 36003	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 36004	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 36005	Lemma for txsconn 36006. (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 36006	The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn)
Theorem	cvxpconn 36007*	A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11280. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ (𝜑 → 𝐾 ∈ PConn)
Theorem	cvxsconn 36008*	A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11280. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ (𝜑 → 𝐾 ∈ SConn)
Theorem	blsconn 36009	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 36010	The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Locally SConn
Theorem	resconn 36011	A subset of ℝ is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ SConn ↔ 𝐽 ∈ Conn))
Theorem	ioosconn 36012	An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((topGen‘ran (,)) ↾t (𝐴(,)𝐵)) ∈ SConn
Theorem	iccsconn 36013	A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ SConn)
Theorem	retopsconn 36014	The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ SConn
Theorem	iccllysconn 36015	A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn)
Theorem	rellysconn 36016	The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ Locally SConn
Theorem	iisconn 36017	The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ II ∈ SConn
Theorem	iillysconn 36018	The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ II ∈ Locally SConn
Theorem	iinllyconn 36019	The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ II ∈ 𝑛-Locally Conn
21.6.8  Covering maps
Syntax	ccvm 36020	Extend class notation with the class of covering maps.
class CovMap
Definition	df-cvm 36021*	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 36022	Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ CovMap Fn (Top × Top)
Theorem	cvmscbv 36023*	Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (◡𝐹 “ 𝑎) ∧ ∀𝑐 ∈ 𝑏 (∀𝑑 ∈ (𝑏 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑎))))})
Theorem	iscvm 36024*	The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) ↔ ((𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ (𝐶 Cn 𝐽)) ∧ ∀𝑥 ∈ 𝑋 ∃𝑘 ∈ 𝐽 (𝑥 ∈ 𝑘 ∧ (𝑆‘𝑘) ≠ ∅)))
Theorem	cvmtop1 36025	Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
Theorem	cvmtop2 36026	Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
Theorem	cvmcn 36027	A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
Theorem	cvmcov 36028*	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 36029*	Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽)
Theorem	cvmsi 36030*	One direction of cvmsval 36031. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈))))))
Theorem	cvmsval 36031*	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 36032*	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 36033*	An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅)
Theorem	cvmsuni 36034*	An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
Theorem	cvmsdisj 36035*	An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	cvmshmeo 36036*	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 36037*	𝐹, 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 36038*	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 36039*	An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅))
Theorem	cvmcov2 36040*	The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑥 ∈ 𝒫 𝑈(𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅))
Theorem	cvmseu 36041*	Every element in ∪ 𝑇 is a member of a unique element of 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥)
Theorem	cvmsiota 36042*	Identify the unique element of 𝑇 containing 𝐴. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑊 = (℩𝑥 ∈ 𝑇 𝐴 ∈ 𝑥)    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊))
Theorem	cvmopnlem 36043*	Lemma for cvmopn 36045. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cvmfolem 36044*	Lemma for cvmfo 36065. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋)
Theorem	cvmopn 36045	A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cvmliftmolem1 36046*	Lemma for cvmliftmo 36049. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))
Theorem	cvmliftmolem2 36047*	Lemma for cvmliftmo 36049. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	cvmliftmoi 36048	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 36049*	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 36050*	Lemma for cvmlift 36064. In cvmliftlem15 36063, 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 36051*	Lemma for cvmlift 36064. 𝑊 = [(𝑘 − 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 36052*	Lemma for cvmlift 36064. 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 36053*	Lemma for cvmlift 36064. 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 36054*	Lemma for cvmlift 36064. 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 36055*	Lemma for cvmlift 36064. Induction step for cvmliftlem7 36056. 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 36056*	Lemma for cvmlift 36064. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 36055 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 36057*	Lemma for cvmlift 36064. 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 36058*	Lemma for cvmlift 36064. 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 36059*	Lemma for cvmlift 36064. 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 36055, cvmliftlem7 36056 (to show it is a function and a lift), cvmliftlem8 36057 (to show it is continuous), and cvmliftlem9 36058 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23612 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 36060*	Lemma for cvmlift 36064. (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 36061*	Lemma for cvmlift 36064. 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 36062*	Lemma for cvmlift 36064. Putting the results of cvmliftlem11 36060, cvmliftlem13 36061 and cvmliftmo 36049 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 36063*	Lemma for cvmlift 36064. Discharge the assumptions of cvmliftlem14 36062. 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 25287, 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 9275 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 36062. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmlift 36064*	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 36050 thru cvmliftlem15 36063. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmfo 36065	A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋)
Theorem	cvmliftiota 36066*	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 36067*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ (∀𝑦 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
Theorem	cvmlift2lem9a 36068*	Lemma for cvmlift2 36081 and cvmlift3 36093. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐻:𝑌⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))    &   ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝑌)    &   ⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊)    ⇒   ⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶))
Theorem	cvmlift2lem2 36069*	Lemma for cvmlift2 36081. (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 36070*	Lemma for cvmlift2 36081. (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 36071*	Lemma for cvmlift2 36081. (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 36072*	Lemma for cvmlift2 36081. (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 36073*	Lemma for cvmlift2 36081. (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 36074*	Lemma for cvmlift2 36081. (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 36075*	Lemma for cvmlift2 36081. (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 36076*	Lemma for cvmlift2 36081. (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 36077*	Lemma for cvmlift2 36081. (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 36078*	Lemma for cvmlift2 36081. (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 𝐶)))    ⇒   ⊢ (𝜑 → ((𝑈 × {𝑌}) ⊆ 𝑀 → (𝑈 × {𝑍}) ⊆ 𝑀))
Theorem	cvmlift2lem12 36079*	Lemma for cvmlift2 36081. (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 𝐶)‘𝑧)}    &   ⊢ 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀}    &   ⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}    ⇒   ⊢ (𝜑 → 𝐾 ∈ ((II ×t II) Cn 𝐶))
Theorem	cvmlift2lem13 36080*	Lemma for cvmlift2 36081. (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) = (𝐻‘𝑥)))‘𝑦))    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃))
Theorem	cvmlift2 36081*	A two-dimensional version of cvmlift 36064. There is a unique lift of functions on the unit square II ×t II which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (0𝑓0) = 𝑃))
Theorem	cvmliftphtlem 36082*	Lemma for cvmliftpht 36083. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑀 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝑁 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐺(PHtpy‘𝐽)𝐻))    &   ⊢ (𝜑 → 𝐴 ∈ ((II ×t II) Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝐴) = 𝐾)    &   ⊢ (𝜑 → (0𝐴0) = 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑀(PHtpy‘𝐶)𝑁))
Theorem	cvmliftpht 36083*	If 𝐺 and 𝐻 are path-homotopic, then their lifts 𝑀 and 𝑁 are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑀 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))    &   ⊢ 𝑁 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    &   ⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐻)    ⇒   ⊢ (𝜑 → 𝑀( ≃ph‘𝐶)𝑁)
Theorem	cvmlift3lem1 36084*	Lemma for cvmlift3 36093. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ (𝜑 → 𝑀 ∈ (II Cn 𝐾))    &   ⊢ (𝜑 → (𝑀‘0) = 𝑂)    &   ⊢ (𝜑 → 𝑁 ∈ (II Cn 𝐾))    &   ⊢ (𝜑 → (𝑁‘0) = 𝑂)    &   ⊢ (𝜑 → (𝑀‘1) = (𝑁‘1))    ⇒   ⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑀) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = 𝑃))‘1))
Theorem	cvmlift3lem2 36085*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ∃!𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))
Theorem	cvmlift3lem3 36086*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    ⇒   ⊢ (𝜑 → 𝐻:𝑌⟶𝐵)
Theorem	cvmlift3lem4 36087*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ((𝐻‘𝑋) = 𝐴 ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝐴)))
Theorem	cvmlift3lem5 36088*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺)
Theorem	cvmlift3lem6 36089*	Lemma for cvmlift3 36093. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))    &   ⊢ (𝜑 → 𝑀 ⊆ (◡𝐺 “ 𝐴))    &   ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑄 ∈ (II Cn 𝐾))    &   ⊢ 𝑅 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑄) ∧ (𝑔‘0) = 𝑃))    &   ⊢ (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻‘𝑋)))    &   ⊢ (𝜑 → 𝑁 ∈ (II Cn (𝐾 ↾t 𝑀)))    &   ⊢ (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍))    &   ⊢ 𝐼 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = (𝐻‘𝑋)))    ⇒   ⊢ (𝜑 → (𝐻‘𝑍) ∈ 𝑊)
Theorem	cvmlift3lem7 36090*	Lemma for cvmlift3 36093. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))    &   ⊢ (𝜑 → 𝑀 ⊆ (◡𝐺 “ 𝐴))    &   ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏)    &   ⊢ (𝜑 → (𝐾 ↾t 𝑀) ∈ PConn)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐻 ∈ ((𝐾 CnP 𝐶)‘𝑋))
Theorem	cvmlift3lem8 36091*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝐾 Cn 𝐶))
Theorem	cvmlift3lem9 36092*	Lemma for cvmlift2 36081. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃))
Theorem	cvmlift3 36093*	A general version of cvmlift 36064. If 𝐾 is simply connected and weakly locally path-connected, then there is a unique lift of functions on 𝐾 which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ (𝐾 Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃))
21.6.9  Normal numbers
Theorem	snmlff 36094*	The function 𝐹 from snmlval 36096 is a mapping from positive integers to real numbers in the range [0, 1]. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((♯‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛))    ⇒   ⊢ 𝐹:ℕ⟶(0[,]1)
Theorem	snmlfval 36095*	The function 𝐹 from snmlval 36096 maps 𝑁 to the relative density of 𝐵 in the first 𝑁 digits of the digit string of 𝐴 in base 𝑅. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((♯‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((♯‘{𝑘 ∈ (1...𝑁) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑁))
Theorem	snmlval 36096*	The property "𝐴 is simply normal in base 𝑅". A number is simply normal if each digit 0 ≤ 𝑏 < 𝑅 occurs in the base- 𝑅 digit string of 𝐴 with frequency 1 / 𝑅 (which is consistent with the expectation in an infinite random string of numbers selected from 0...𝑅 − 1). (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑆 = (𝑟 ∈ (ℤ≥‘2) ↦ {𝑥 ∈ ℝ ∣ ∀𝑏 ∈ (0...(𝑟 − 1))(𝑛 ∈ ℕ ↦ ((♯‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝑥 · (𝑟↑𝑘)) mod 𝑟)) = 𝑏}) / 𝑛)) ⇝ (1 / 𝑟)})    ⇒   ⊢ (𝐴 ∈ (𝑆‘𝑅) ↔ (𝑅 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ ∧ ∀𝑏 ∈ (0...(𝑅 − 1))(𝑛 ∈ ℕ ↦ ((♯‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝑏}) / 𝑛)) ⇝ (1 / 𝑅)))
Theorem	snmlflim 36097*	If 𝐴 is simply normal, then the function 𝐹 of relative density of 𝐵 in the digit string converges to 1 / 𝑅, i.e. the set of occurrences of 𝐵 in the digit string has natural density 1 / 𝑅. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ 𝑆 = (𝑟 ∈ (ℤ≥‘2) ↦ {𝑥 ∈ ℝ ∣ ∀𝑏 ∈ (0...(𝑟 − 1))(𝑛 ∈ ℕ ↦ ((♯‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝑥 · (𝑟↑𝑘)) mod 𝑟)) = 𝑏}) / 𝑛)) ⇝ (1 / 𝑟)})    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((♯‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛))    ⇒   ⊢ ((𝐴 ∈ (𝑆‘𝑅) ∧ 𝐵 ∈ (0...(𝑅 − 1))) → 𝐹 ⇝ (1 / 𝑅))
21.6.10  Godel-sets of formulas - part 1
Syntax	cgoe 36098	The Godel-set of membership.
class ∈𝑔
Syntax	cgna 36099	The Godel-set for the Sheffer stroke.
class ⊼𝑔
Syntax	cgol 36100	The Godel-set of universal quantification. (Note that this is not a wff.)
class ∀𝑔𝑁𝑈