Home | Metamath
Proof Explorer Theorem List (p. 325 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fncvm 32401 | Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ CovMap Fn (Top × Top) | ||
Theorem | cvmscbv 32402* | Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (◡𝐹 “ 𝑎) ∧ ∀𝑐 ∈ 𝑏 (∀𝑑 ∈ (𝑏 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑎))))}) | ||
Theorem | iscvm 32403* | The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) ↔ ((𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ (𝐶 Cn 𝐽)) ∧ ∀𝑥 ∈ 𝑋 ∃𝑘 ∈ 𝐽 (𝑥 ∈ 𝑘 ∧ (𝑆‘𝑘) ≠ ∅))) | ||
Theorem | cvmtop1 32404 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) | ||
Theorem | cvmtop2 32405 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top) | ||
Theorem | cvmcn 32406 | A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) | ||
Theorem | cvmcov 32407* | 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 32408* | Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽) | ||
Theorem | cvmsi 32409* | One direction of cvmsval 32410. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈)))))) | ||
Theorem | cvmsval 32410* | 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 32411* | 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 32412* | An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅) | ||
Theorem | cvmsuni 32413* | An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) | ||
Theorem | cvmsdisj 32414* | An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
Theorem | cvmshmeo 32415* | 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 32416* | 𝐹, 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 32417* | 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 32418* | An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅)) | ||
Theorem | cvmcov2 32419* | The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑥 ∈ 𝒫 𝑈(𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅)) | ||
Theorem | cvmseu 32420* | Every element in ∪ 𝑇 is a member of a unique element of 𝑇. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) | ||
Theorem | cvmsiota 32421* | Identify the unique element of 𝑇 containing 𝐴. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑊 = (℩𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝑊 ∈ 𝑇 ∧ 𝐴 ∈ 𝑊)) | ||
Theorem | cvmopnlem 32422* | Lemma for cvmopn 32424. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽) | ||
Theorem | cvmfolem 32423* | Lemma for cvmfo 32444. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋) | ||
Theorem | cvmopn 32424 | A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽) | ||
Theorem | cvmliftmolem1 32425* | Lemma for cvmliftmo 32428. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn) & ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼) & ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁))) | ||
Theorem | cvmliftmolem2 32426* | Lemma for cvmliftmo 32428. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Conn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Conn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) & ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) & ⊢ (𝜑 → (𝑀‘𝑂) = (𝑁‘𝑂)) & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
Theorem | cvmliftmoi 32427 | 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 32428* | 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 32429* | Lemma for cvmlift 32443. In cvmliftlem15 32442, 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 32430* | Lemma for cvmlift 32443. 𝑊 = [(𝑘 − 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 32431* | Lemma for cvmlift 32443. 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 32432* | Lemma for cvmlift 32443. 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 32433* | Lemma for cvmlift 32443. 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 32434* | Lemma for cvmlift 32443. Induction step for cvmliftlem7 32435. 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 32435* | Lemma for cvmlift 32443. Prove by induction that every 𝑄 function is well-defined (we can immediately follow this theorem with cvmliftlem6 32434 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 32436* | Lemma for cvmlift 32443. 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 32437* | Lemma for cvmlift 32443. 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 32438* | Lemma for cvmlift 32443. 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 32434, cvmliftlem7 32435 (to show it is a function and a lift), cvmliftlem8 32436 (to show it is continuous), and cvmliftlem9 32437 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 21830 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 32439* | Lemma for cvmlift 32443. (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 32440* | Lemma for cvmlift 32443. 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 32441* | Lemma for cvmlift 32443. Putting the results of cvmliftlem11 32439, cvmliftlem13 32440 and cvmliftmo 32428 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 32442* | Lemma for cvmlift 32443. Discharge the assumptions of cvmliftlem14 32441. 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 23497, 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 8750 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 32441. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) ⇒ ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) | ||
Theorem | cvmlift 32443* | 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 32429 thru cvmliftlem15 32442. (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) | ||
Theorem | cvmfo 32444 | A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋) | ||
Theorem | cvmliftiota 32445* | 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 32446* | Lemma for cvmlift2 32460. (Contributed by Mario Carneiro, 1-Jun-2015.) |
⊢ (∀𝑦 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀)) | ||
Theorem | cvmlift2lem9a 32447* | Lemma for cvmlift2 32460 and cvmlift3 32472. (Contributed by Mario Carneiro, 9-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐻:𝑌⟶𝐵) & ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) & ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) & ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) & ⊢ (𝜑 → 𝑀 ⊆ 𝑌) & ⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊) ⇒ ⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶)) | ||
Theorem | cvmlift2lem2 32448* | Lemma for cvmlift2 32460. (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 32449* | Lemma for cvmlift2 32460. (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 32450* | Lemma for cvmlift2 32460. (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 32451* | Lemma for cvmlift2 32460. (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 32452* | Lemma for cvmlift2 32460. (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 32453* | Lemma for cvmlift2 32460. (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 32454* | Lemma for cvmlift2 32460. (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 32455* | Lemma for cvmlift2 32460. (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 32456* | Lemma for cvmlift2 32460. (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 32457* | Lemma for cvmlift2 32460. (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 32458* | Lemma for cvmlift2 32460. (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 32459* | Lemma for cvmlift2 32460. (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 32460* | A two-dimensional version of cvmlift 32443. 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 32461* | Lemma for cvmliftpht 32462. (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 32462* | 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 32463* | Lemma for cvmlift3 32472. (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 32464* | Lemma for cvmlift2 32460. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ∃!𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)) | ||
Theorem | cvmlift3lem3 32465* | Lemma for cvmlift2 32460. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) & ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) ⇒ ⊢ (𝜑 → 𝐻:𝑌⟶𝐵) | ||
Theorem | cvmlift3lem4 32466* | Lemma for cvmlift2 32460. (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 32467* | Lemma for cvmlift2 32460. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) & ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) | ||
Theorem | cvmlift3lem6 32468* | Lemma for cvmlift3 32472. (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 32469* | Lemma for cvmlift3 32472. (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 32470* | Lemma for cvmlift2 32460. (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 32471* | Lemma for cvmlift2 32460. (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 32472* | A general version of cvmlift 32443. 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 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘𝑂) = 𝑃)) | ||
Theorem | snmlff 32473* | The function 𝐹 from snmlval 32475 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 32474* | The function 𝐹 from snmlval 32475 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 32475* | 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 32476* | 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 / 𝑅)) | ||
Syntax | cgoe 32477 | The Godel-set of membership. |
class ∈𝑔 | ||
Syntax | cgna 32478 | The Godel-set for the Sheffer stroke. |
class ⊼𝑔 | ||
Syntax | cgol 32479 | The Godel-set of universal quantification. (Note that this is not a wff.) |
class ∀𝑔𝑁𝑈 | ||
Syntax | csat 32480 | The satisfaction function. |
class Sat | ||
Syntax | cfmla 32481 | The formula set predicate. |
class Fmla | ||
Syntax | csate 32482 | The ∈-satisfaction function. |
class Sat∈ | ||
Syntax | cprv 32483 | The "proves" relation. |
class ⊧ | ||
Definition | df-goel 32484 | 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 32485 | 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 32486 | 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 32487* |
Define the satisfaction predicate. This recursive construction builds up
a function over wff codes (see satff 32554) 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
(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 32488* | 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 32489 | 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 32487 for the full coding scheme), see fmla0 32526, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 32530. 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 32588. (Fmla‘ω) = ∪ 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 32525. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛)) | ||
Definition | df-prv 32490* | 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 32574 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 32491 | 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 32492 | A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023.) |
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ (ω × (ω × ω))) | ||
Theorem | goeleq12bg 32493 | 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 32494 | The "Godel-set for the Sheffer stroke NAND" for two formulas 𝐴 and 𝐵. (Contributed by AV, 16-Oct-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴⊼𝑔𝐵) = 〈1o, 〈𝐴, 𝐵〉〉) | ||
Theorem | goaleq12d 32495 | Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023.) |
⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∀𝑔𝑀𝐴 = ∀𝑔𝑁𝐵) | ||
Theorem | gonanegoal 32496 | 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 32497* | 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 32498* | 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 32499 | 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 32500* | The satisfaction predicate for wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 at omega (ω). (Contributed by AV, 6-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘ω) = ∪ 𝑛 ∈ ω ((𝑀 Sat 𝐸)‘𝑛)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |