P. 356 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cvmsval 35501*	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 35502*	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 35503*	An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅)
Theorem	cvmsuni 35504*	An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
Theorem	cvmsdisj 35505*	An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	cvmshmeo 35506*	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 35507*	𝐹, 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 35508*	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 35509*	An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅))
Theorem	cvmcov2 35510*	The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑥 ∈ 𝒫 𝑈(𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅))
Theorem	cvmseu 35511*	Every element in ∪ 𝑇 is a member of a unique element of 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥)
Theorem	cvmsiota 35512*	Identify the unique element of 𝑇 containing 𝐴. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑊 = (℩𝑥 ∈ 𝑇 𝐴 ∈ 𝑥)    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊))
Theorem	cvmopnlem 35513*	Lemma for cvmopn 35515. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cvmfolem 35514*	Lemma for cvmfo 35535. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋)
Theorem	cvmopn 35515	A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cvmliftmolem1 35516*	Lemma for cvmliftmo 35519. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))
Theorem	cvmliftmolem2 35517*	Lemma for cvmliftmo 35519. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Conn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))    &   ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))    &   ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂))    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	cvmliftmoi 35518	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 35519*	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 35520*	Lemma for cvmlift 35534. In cvmliftlem15 35533, 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 35521*	Lemma for cvmlift 35534. 𝑊 = [(𝑘 − 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 35522*	Lemma for cvmlift 35534. 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 35523*	Lemma for cvmlift 35534. 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 35524*	Lemma for cvmlift 35534. 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 35525*	Lemma for cvmlift 35534. Induction step for cvmliftlem7 35526. 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 35526*	Lemma for cvmlift 35534. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 35525 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 35527*	Lemma for cvmlift 35534. 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 35528*	Lemma for cvmlift 35534. 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 35529*	Lemma for cvmlift 35534. 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 35525, cvmliftlem7 35526 (to show it is a function and a lift), cvmliftlem8 35527 (to show it is continuous), and cvmliftlem9 35528 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23284 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 35530*	Lemma for cvmlift 35534. (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 35531*	Lemma for cvmlift 35534. 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 35532*	Lemma for cvmlift 35534. Putting the results of cvmliftlem11 35530, cvmliftlem13 35531 and cvmliftmo 35519 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 35533*	Lemma for cvmlift 35534. Discharge the assumptions of cvmliftlem14 35532. 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 24958, 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 9191 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 35532. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmlift 35534*	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 35520 thru cvmliftlem15 35533. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    ⇒   ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
Theorem	cvmfo 35535	A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋)
Theorem	cvmliftiota 35536*	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 35537*	Lemma for cvmlift2 35551. (Contributed by Mario Carneiro, 1-Jun-2015.)
⊢ (∀𝑦 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
Theorem	cvmlift2lem9a 35538*	Lemma for cvmlift2 35551 and cvmlift3 35563. (Contributed by Mario Carneiro, 9-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐻:𝑌⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ Top)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))    &   ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊))    &   ⊢ (𝜑 → 𝑀 ⊆ 𝑌)    &   ⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊)    ⇒   ⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶))
Theorem	cvmlift2lem2 35539*	Lemma for cvmlift2 35551. (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 35540*	Lemma for cvmlift2 35551. (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 35541*	Lemma for cvmlift2 35551. (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 35542*	Lemma for cvmlift2 35551. (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 35543*	Lemma for cvmlift2 35551. (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 35544*	Lemma for cvmlift2 35551. (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 35545*	Lemma for cvmlift2 35551. (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 35546*	Lemma for cvmlift2 35551. (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 35547*	Lemma for cvmlift2 35551. (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 35548*	Lemma for cvmlift2 35551. (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 35549*	Lemma for cvmlift2 35551. (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 35550*	Lemma for cvmlift2 35551. (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 35551*	A two-dimensional version of cvmlift 35534. 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 35552*	Lemma for cvmliftpht 35553. (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 35553*	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 35554*	Lemma for cvmlift3 35563. (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 35555*	Lemma for cvmlift2 35551. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ∃!𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))
Theorem	cvmlift3lem3 35556*	Lemma for cvmlift2 35551. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    ⇒   ⊢ (𝜑 → 𝐻:𝑌⟶𝐵)
Theorem	cvmlift3lem4 35557*	Lemma for cvmlift2 35551. (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 35558*	Lemma for cvmlift2 35551. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ 𝐵 = ∪ 𝐶    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))    &   ⊢ (𝜑 → 𝐾 ∈ SConn)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺)
Theorem	cvmlift3lem6 35559*	Lemma for cvmlift3 35563. (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 35560*	Lemma for cvmlift3 35563. (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 35561*	Lemma for cvmlift2 35551. (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 35562*	Lemma for cvmlift2 35551. (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 35563*	A general version of cvmlift 35534. 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 35564*	The function 𝐹 from snmlval 35566 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 35565*	The function 𝐹 from snmlval 35566 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 35566*	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 35567*	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 35568	The Godel-set of membership.
class ∈𝑔
Syntax	cgna 35569	The Godel-set for the Sheffer stroke.
class ⊼𝑔
Syntax	cgol 35570	The Godel-set of universal quantification. (Note that this is not a wff.)
class ∀𝑔𝑁𝑈
Syntax	csat 35571	The satisfaction function.
class Sat
Syntax	cfmla 35572	The formula set predicate.
class Fmla
Syntax	csate 35573	The ∈-satisfaction function.
class Sat∈
Syntax	cprv 35574	The "proves" relation.
class ⊧
Definition	df-goel 35575	Define the Godel-set of membership. Here the arguments 𝑥 = ⟨𝑁, 𝑃⟩ correspond to vN and vP , so (∅∈𝑔1o) actually means v0 ∈ v1 , not 0 ∈ 1. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ ∈𝑔 = (𝑥 ∈ (ω × ω) ↦ ⟨∅, 𝑥⟩)
Definition	df-gona 35576	Define the Godel-set for the Sheffer stroke NAND. Here the arguments 𝑥 = ⟨𝑈, 𝑉⟩ are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ ⊼𝑔 = (𝑥 ∈ (V × V) ↦ ⟨1o, 𝑥⟩)
Definition	df-goal 35577	Define the Godel-set of universal quantification. Here 𝑁 ∈ ω corresponds to vN , and 𝑈 represents another formula, and this expression is [∀𝑥𝜑] = ∀𝑔𝑁𝑈 where 𝑥 is the 𝑁-th variable, 𝑈 = [𝜑] is the code for 𝜑. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ ∀𝑔𝑁𝑈 = ⟨2o, ⟨𝑁, 𝑈⟩⟩
Definition	df-sat 35578*	Define the satisfaction predicate. This recursive construction builds up a function over wff codes (see satff 35645) and simultaneously defines the set of assignments to all variables from 𝑀 that makes the coded wff true in the model 𝑀, where ∈ is interpreted as the binary relation 𝐸 on 𝑀. The interpretation of the statement 𝑆 ∈ (((𝑀 Sat 𝐸)‘𝑛)‘𝑈) is that for the model ⟨𝑀, 𝐸⟩, 𝑆:ω⟶𝑀 is a valuation of the variables (v0 = (𝑆‘∅), v1 = (𝑆‘1o), etc.) and 𝑈 is a code for a wff using ∈ , ⊼ , ∀ that is true under the assignment 𝑆. The function is defined by finite recursion; ((𝑀 Sat 𝐸)‘𝑛) only operates on wffs of depth at most 𝑛 ∈ ω, and ((𝑀 Sat 𝐸)‘ω) = ∪ 𝑛 ∈ ω((𝑀 Sat 𝐸)‘𝑛) operates on all wffs. The coding scheme for the wffs is defined so that vi ∈ vj is coded as ⟨∅, ⟨𝑖, 𝑗⟩⟩, (𝜑 ⊼ 𝜓) is coded as ⟨1o, ⟨𝜑, 𝜓⟩⟩, and ∀ vi 𝜑 is coded as ⟨2o, ⟨𝑖, 𝜑⟩⟩. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ Sat = (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω))
Definition	df-sate 35579*	A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable 𝑛. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ Sat∈ = (𝑚 ∈ V, 𝑢 ∈ V ↦ (((𝑚 Sat ( E ∩ (𝑚 × 𝑚)))‘ω)‘𝑢))
Definition	df-fmla 35580	Define the predicate which defines the set of valid Godel formulas. The parameter 𝑛 defines the maximum height of the formulas: the set (Fmla‘∅) is all formulas of the form 𝑥 ∈ 𝑦 (which in our coding scheme is the set ({∅} × (ω × ω)); see df-sat 35578 for the full coding scheme), see fmla0 35617, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 35621. Remark: it is sufficient to have atomic formulas of the form 𝑥 ∈ 𝑦 only, because equations (formulas of the form 𝑥 = 𝑦), which are required as (atomic) formulas, can be introduced as a defined notion in terms of ∈𝑔, see df-goeq 35679. (Fmla‘ω) = ∪ 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 35616. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))
Definition	df-prv 35581*	Define the "proves" relation on a set. A wff is true in a model 𝑀 if for every valuation 𝑠 ∈ (𝑀 ↑m ω), the interpretation of the wff using the membership relation on 𝑀 is true. Since ⊧ is defined in terms of the interpretations making the given formula true, it is not defined on the empty "model" 𝑀 = ∅, since there are no interpretations. In particular, the empty set on the LHS of ⊧ should not be interpreted as the empty model. Statement prv0 35665 shows that our definition yields ∅⊧𝑈 for all formulas, though of course the formula ∃𝑥𝑥 = 𝑥 is not satisfied on the empty model. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ ⊧ = {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)}
Theorem	goel 35582	A "Godel-set of membership". The variables are identified by their indices (which are natural numbers), and the membership vi ∈ vj is coded as ⟨∅, ⟨𝑖, 𝑗⟩⟩. (Contributed by AV, 15-Sep-2023.)
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) = ⟨∅, ⟨𝐼, 𝐽⟩⟩)
Theorem	goelel3xp 35583	A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023.)
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ (ω × (ω × ω)))
Theorem	goeleq12bg 35584	Two "Godel-set of membership" codes for two variables are equal iff the two corresponding variables are equal. (Contributed by AV, 8-Oct-2023.)
⊢ (((𝑀 ∈ ω ∧ 𝑁 ∈ ω) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω)) → ((𝐼∈𝑔𝐽) = (𝑀∈𝑔𝑁) ↔ (𝐼 = 𝑀 ∧ 𝐽 = 𝑁)))
Theorem	gonafv 35585	The "Godel-set for the Sheffer stroke NAND" for two formulas 𝐴 and 𝐵. (Contributed by AV, 16-Oct-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴⊼𝑔𝐵) = ⟨1o, ⟨𝐴, 𝐵⟩⟩)
Theorem	goaleq12d 35586	Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∀𝑔𝑀𝐴 = ∀𝑔𝑁𝐵)
Theorem	gonanegoal 35587	The Godel-set for the Sheffer stroke NAND is not equal to the Godel-set of universal quantification. (Contributed by AV, 21-Oct-2023.)
⊢ (𝑎⊼𝑔𝑏) ≠ ∀𝑔𝑖𝑢
Theorem	satf 35588*	The satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀. (Contributed by AV, 14-Sep-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑀 Sat 𝐸) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) ↾ suc ω))
Theorem	satfsucom 35589*	The satisfaction predicate for wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 at an element of the successor of ω. (Contributed by AV, 22-Sep-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ suc ω) → ((𝑀 Sat 𝐸)‘𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘𝑁))
Theorem	satfn 35590	The satisfaction predicate for wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 is a function over suc ω. (Contributed by AV, 6-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑀 Sat 𝐸) Fn suc ω)
Theorem	satom 35591*	The satisfaction predicate for wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 at omega (ω). (Contributed by AV, 6-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘ω) = ∪ 𝑛 ∈ ω ((𝑀 Sat 𝐸)‘𝑛))
Theorem	satfvsucom 35592*	The satisfaction predicate as function over wff codes at a successor of ω. (Contributed by AV, 22-Sep-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ suc ω) → (𝑆‘𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})‘𝑁))
Theorem	satfv0 35593*	The value of the satisfaction predicate as function over wff codes at ∅. (Contributed by AV, 8-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
Theorem	satfvsuclem1 35594*	Lemma 1 for satfvsuc 35596. (Contributed by AV, 8-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑m ω))} ∈ V)
Theorem	satfvsuclem2 35595*	Lemma 2 for satfvsuc 35596. (Contributed by AV, 8-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ∈ V)
Theorem	satfvsuc 35596*	The value of the satisfaction predicate as function over wff codes at a successor. (Contributed by AV, 10-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑆‘suc 𝑁) = ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
Theorem	satfv1lem 35597*	Lemma for satfv1 35598. (Contributed by AV, 9-Nov-2023.)
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑁, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))})
Theorem	satfv1 35598*	The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))
Theorem	satfsschain 35599	The binary relation of a satisfaction predicate as function over wff codes is an increasing chain (with respect to inclusion). (Contributed by AV, 15-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐵 ⊆ 𝐴 → (𝑆‘𝐵) ⊆ (𝑆‘𝐴)))
Theorem	satfvsucsuc 35600*	The satisfaction predicate as function over wff codes of height (𝑁 + 1), expressed by the minimally necessary satisfaction predicates as function over wff codes of height 𝑁. (Contributed by AV, 21-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    &   ⊢ 𝐴 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))    &   ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑆‘suc suc 𝑁) = ((𝑆‘suc 𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = 𝐴))}))