| Metamath
Proof Explorer Theorem List (p. 354 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cvmliftlem13 35301* | Lemma for cvmlift 35304. 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 35302* | Lemma for cvmlift 35304. Putting the results of cvmliftlem11 35300, cvmliftlem13 35301 and cvmliftmo 35289 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 35303* | Lemma for cvmlift 35304. Discharge the assumptions of cvmliftlem14 35302. 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 24998, 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 9320 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 35302. (Contributed by Mario Carneiro, 14-Feb-2015.) |
| ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) ⇒ ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) | ||
| Theorem | cvmlift 35304* | 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 35290 thru cvmliftlem15 35303. (Contributed by Mario Carneiro, 16-Feb-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 ⇒ ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) | ||
| Theorem | cvmfo 35305 | A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹:𝐵–onto→𝑋) | ||
| Theorem | cvmliftiota 35306* | 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 35307* | Lemma for cvmlift2 35321. (Contributed by Mario Carneiro, 1-Jun-2015.) |
| ⊢ (∀𝑦 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑦})((𝑢 × {𝑥}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑥}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀)) | ||
| Theorem | cvmlift2lem9a 35308* | Lemma for cvmlift2 35321 and cvmlift3 35333. (Contributed by Mario Carneiro, 9-Jul-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐻:𝑌⟶𝐵) & ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) & ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴)) & ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊)) & ⊢ (𝜑 → 𝑀 ⊆ 𝑌) & ⊢ (𝜑 → (𝐻 “ 𝑀) ⊆ 𝑊) ⇒ ⊢ (𝜑 → (𝐻 ↾ 𝑀) ∈ ((𝐾 ↾t 𝑀) Cn 𝐶)) | ||
| Theorem | cvmlift2lem2 35309* | Lemma for cvmlift2 35321. (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 35310* | Lemma for cvmlift2 35321. (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 35311* | Lemma for cvmlift2 35321. (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 35312* | Lemma for cvmlift2 35321. (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 35313* | Lemma for cvmlift2 35321. (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 35314* | Lemma for cvmlift2 35321. (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 35315* | Lemma for cvmlift2 35321. (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 35316* | Lemma for cvmlift2 35321. (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 35317* | Lemma for cvmlift2 35321. (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 35318* | Lemma for cvmlift2 35321. (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 35319* | Lemma for cvmlift2 35321. (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 35320* | Lemma for cvmlift2 35321. (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 35321* | A two-dimensional version of cvmlift 35304. 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 35322* | Lemma for cvmliftpht 35323. (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 35323* | 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 35324* | Lemma for cvmlift3 35333. (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 35325* | Lemma for cvmlift2 35321. (Contributed by Mario Carneiro, 6-Jul-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ∃!𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)) | ||
| Theorem | cvmlift3lem3 35326* | Lemma for cvmlift2 35321. (Contributed by Mario Carneiro, 6-Jul-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) & ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) ⇒ ⊢ (𝜑 → 𝐻:𝑌⟶𝐵) | ||
| Theorem | cvmlift3lem4 35327* | Lemma for cvmlift2 35321. (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 35328* | Lemma for cvmlift2 35321. (Contributed by Mario Carneiro, 6-Jul-2015.) |
| ⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) & ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) | ||
| Theorem | cvmlift3lem6 35329* | Lemma for cvmlift3 35333. (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 35330* | Lemma for cvmlift3 35333. (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 35331* | Lemma for cvmlift2 35321. (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 35332* | Lemma for cvmlift2 35321. (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 35333* | A general version of cvmlift 35304. 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 35334* | The function 𝐹 from snmlval 35336 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 35335* | The function 𝐹 from snmlval 35336 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 35336* | 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 35337* | 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 35338 | The Godel-set of membership. |
| class ∈𝑔 | ||
| Syntax | cgna 35339 | The Godel-set for the Sheffer stroke. |
| class ⊼𝑔 | ||
| Syntax | cgol 35340 | The Godel-set of universal quantification. (Note that this is not a wff.) |
| class ∀𝑔𝑁𝑈 | ||
| Syntax | csat 35341 | The satisfaction function. |
| class Sat | ||
| Syntax | cfmla 35342 | The formula set predicate. |
| class Fmla | ||
| Syntax | csate 35343 | The ∈-satisfaction function. |
| class Sat∈ | ||
| Syntax | cprv 35344 | The "proves" relation. |
| class ⊧ | ||
| Definition | df-goel 35345 | 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 35346 | 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 35347 | 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 35348* |
Define the satisfaction predicate. This recursive construction builds up
a function over wff codes (see satff 35415) 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 35349* | 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 35350 | 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 35348 for the full coding scheme), see fmla0 35387, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 35391. 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 35449. (Fmla‘ω) = ∪ 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 35386. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛)) | ||
| Definition | df-prv 35351* | 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 35435 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 35352 | 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 35353 | A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023.) |
| ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ (ω × (ω × ω))) | ||
| Theorem | goeleq12bg 35354 | 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 35355 | The "Godel-set for the Sheffer stroke NAND" for two formulas 𝐴 and 𝐵. (Contributed by AV, 16-Oct-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴⊼𝑔𝐵) = 〈1o, 〈𝐴, 𝐵〉〉) | ||
| Theorem | goaleq12d 35356 | Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023.) |
| ⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∀𝑔𝑀𝐴 = ∀𝑔𝑁𝐵) | ||
| Theorem | gonanegoal 35357 | 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 35358* | 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 35359* | 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 35360 | 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 35361* | 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 35362* | 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 35363* | The value of the satisfaction predicate as function over wff codes at ∅. (Contributed by AV, 8-Oct-2023.) |
| ⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) | ||
| Theorem | satfvsuclem1 35364* | Lemma 1 for satfvsuc 35366. (Contributed by AV, 8-Oct-2023.) |
| ⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑m ω))} ∈ V) | ||
| Theorem | satfvsuclem2 35365* | Lemma 2 for satfvsuc 35366. (Contributed by AV, 8-Oct-2023.) |
| ⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ∈ V) | ||
| Theorem | satfvsuc 35366* | 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 35367* | Lemma for satfv1 35368. (Contributed by AV, 9-Nov-2023.) |
| ⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}) | ||
| Theorem | satfv1 35368* | 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 35369 | 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 35370* | 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 ‘𝑣)) ∧ 𝑦 = 𝐴))})) | ||
| Theorem | satfbrsuc 35371* | The binary relation of a satisfaction predicate as function over wff codes at a successor. (Contributed by AV, 13-Oct-2023.) |
| ⊢ 𝑆 = (𝑀 Sat 𝐸) & ⊢ 𝑃 = (𝑆‘𝑁) ⇒ ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑁 ∈ ω ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴(𝑆‘suc 𝑁)𝐵 ↔ (𝐴𝑃𝐵 ∨ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))) | ||
| Theorem | satfrel 35372 | The value of the satisfaction predicate as function over wff codes at a natural number is a relation. (Contributed by AV, 12-Oct-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁)) | ||
| Theorem | satfdmlem 35373* | Lemma for satfdm 35374. (Contributed by AV, 12-Oct-2023.) |
| ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st ‘𝑎)⊼𝑔(1st ‘𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑎)))) | ||
| Theorem | satfdm 35374* | The domain of the satisfaction predicate as function over wff codes does not depend on the model 𝑀 and the binary relation 𝐸 on 𝑀. (Contributed by AV, 13-Oct-2023.) |
| ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌)) → ∀𝑛 ∈ ω dom ((𝑀 Sat 𝐸)‘𝑛) = dom ((𝑁 Sat 𝐹)‘𝑛)) | ||
| Theorem | satfrnmapom 35375 | The range of the satisfaction predicate as function over wff codes in any model 𝑀 and any binary relation 𝐸 on 𝑀 for a natural number 𝑁 is a subset of the power set of all mappings from the natural numbers into the model 𝑀. (Contributed by AV, 13-Oct-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → ran ((𝑀 Sat 𝐸)‘𝑁) ⊆ 𝒫 (𝑀 ↑m ω)) | ||
| Theorem | satfv0fun 35376 | The value of the satisfaction predicate as function over wff codes at ∅ is a function. (Contributed by AV, 15-Oct-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘∅)) | ||
| Theorem | satf0 35377* | The satisfaction predicate as function over wff codes in the empty model with an empty binary relation. (Contributed by AV, 14-Sep-2023.) |
| ⊢ (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) ↾ suc ω) | ||
| Theorem | satf0sucom 35378* | The satisfaction predicate as function over wff codes in the empty model with an empty binary relation at a successor of ω. (Contributed by AV, 14-Sep-2023.) |
| ⊢ (𝑁 ∈ suc ω → ((∅ Sat ∅)‘𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) | ||
| Theorem | satf00 35379* | The value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at ∅. (Contributed by AV, 14-Sep-2023.) |
| ⊢ ((∅ Sat ∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} | ||
| Theorem | satf0suclem 35380* | Lemma for satf0suc 35381, sat1el2xp 35384 and fmlasuc0 35389. (Contributed by AV, 19-Sep-2023.) |
| ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑋 (∃𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃𝑤 ∈ 𝑍 𝑥 = 𝐶))} ∈ V) | ||
| Theorem | satf0suc 35381* | The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation at a successor. (Contributed by AV, 19-Sep-2023.) |
| ⊢ 𝑆 = (∅ Sat ∅) ⇒ ⊢ (𝑁 ∈ ω → (𝑆‘suc 𝑁) = ((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})) | ||
| Theorem | satf0op 35382* | An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023.) |
| ⊢ 𝑆 = (∅ Sat ∅) ⇒ ⊢ (𝑁 ∈ ω → (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = 〈𝑥, ∅〉 ∧ 〈𝑥, ∅〉 ∈ (𝑆‘𝑁)))) | ||
| Theorem | satf0n0 35383 | The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation does not contain the empty set. (Contributed by AV, 19-Sep-2023.) |
| ⊢ (𝑁 ∈ ω → ∅ ∉ ((∅ Sat ∅)‘𝑁)) | ||
| Theorem | sat1el2xp 35384* | The first component of an element of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation is a member of a doubled Cartesian product. (Contributed by AV, 17-Sep-2023.) |
| ⊢ (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) | ||
| Theorem | fmlafv 35385 | The valid Godel formulas of height 𝑁 is the domain of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at 𝑁. (Contributed by AV, 15-Sep-2023.) |
| ⊢ (𝑁 ∈ suc ω → (Fmla‘𝑁) = dom ((∅ Sat ∅)‘𝑁)) | ||
| Theorem | fmla 35386 | The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023.) |
| ⊢ (Fmla‘ω) = ∪ 𝑛 ∈ ω (Fmla‘𝑛) | ||
| Theorem | fmla0 35387* | The valid Godel formulas of height 0 is the set of all formulas of the form vi ∈ vj ("Godel-set of membership") coded as 〈∅, 〈𝑖, 𝑗〉〉. (Contributed by AV, 14-Sep-2023.) |
| ⊢ (Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} | ||
| Theorem | fmla0xp 35388 | The valid Godel formulas of height 0 is the set of all formulas of the form vi ∈ vj ("Godel-set of membership") coded as 〈∅, 〈𝑖, 𝑗〉〉. (Contributed by AV, 15-Sep-2023.) |
| ⊢ (Fmla‘∅) = ({∅} × (ω × ω)) | ||
| Theorem | fmlasuc0 35389* | The valid Godel formulas of height (𝑁 + 1). (Contributed by AV, 18-Sep-2023.) |
| ⊢ (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))})) | ||
| Theorem | fmlafvel 35390 | A class is a valid Godel formula of height 𝑁 iff it is the first component of a member of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at 𝑁. (Contributed by AV, 19-Sep-2023.) |
| ⊢ (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat ∅)‘𝑁))) | ||
| Theorem | fmlasuc 35391* | The valid Godel formulas of height (𝑁 + 1), expressed by the valid Godel formulas of height 𝑁. (Contributed by AV, 20-Sep-2023.) |
| ⊢ (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) | ||
| Theorem | fmla1 35392* | The valid Godel formulas of height 1 is the set of all formulas of the form (𝑎⊼𝑔𝑏) and ∀𝑔𝑘𝑎 with atoms 𝑎, 𝑏 of the form 𝑥 ∈ 𝑦. (Contributed by AV, 20-Sep-2023.) |
| ⊢ (Fmla‘1o) = (({∅} × (ω × ω)) ∪ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑙 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))}) | ||
| Theorem | isfmlasuc 35393* | The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023.) |
| ⊢ ((𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ (Fmla‘suc 𝑁) ↔ (𝐹 ∈ (Fmla‘𝑁) ∨ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝐹 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝐹 = ∀𝑔𝑖𝑢)))) | ||
| Theorem | fmlasssuc 35394 | The Godel formulas of height 𝑁 are a subset of the Godel formulas of height 𝑁 + 1. (Contributed by AV, 20-Oct-2023.) |
| ⊢ (𝑁 ∈ ω → (Fmla‘𝑁) ⊆ (Fmla‘suc 𝑁)) | ||
| Theorem | fmlaomn0 35395 | The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.) |
| ⊢ (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁)) | ||
| Theorem | fmlan0 35396 | The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023.) |
| ⊢ ∅ ∉ (Fmla‘ω) | ||
| Theorem | gonan0 35397 | The "Godel-set of NAND" is a Godel formula of at least height 1. (Contributed by AV, 21-Oct-2023.) |
| ⊢ ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) | ||
| Theorem | goaln0 35398* | The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023.) |
| ⊢ (∀𝑔𝑖𝐴 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) | ||
| Theorem | gonarlem 35399* | Lemma for gonar 35400 (induction step). (Contributed by AV, 21-Oct-2023.) |
| ⊢ (𝑁 ∈ ω → (((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc 𝑁) → (𝑎 ∈ (Fmla‘suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc 𝑁))) → ((𝑎⊼𝑔𝑏) ∈ (Fmla‘suc suc 𝑁) → (𝑎 ∈ (Fmla‘suc suc 𝑁) ∧ 𝑏 ∈ (Fmla‘suc suc 𝑁))))) | ||
| Theorem | gonar 35400* | If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for 𝐴 or 𝐵 being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023.) |
| ⊢ ((𝑁 ∈ ω ∧ (𝑎⊼𝑔𝑏) ∈ (Fmla‘𝑁)) → (𝑎 ∈ (Fmla‘𝑁) ∧ 𝑏 ∈ (Fmla‘𝑁))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |