![]() |
Metamath
Proof Explorer Theorem List (p. 354 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cvmliftphtlem 35301* | Lemma for cvmliftpht 35302. (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 35302* | 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 35303* | Lemma for cvmlift3 35312. (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 35304* | Lemma for cvmlift2 35300. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑌) → ∃!𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑋 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)) | ||
Theorem | cvmlift3lem3 35305* | Lemma for cvmlift2 35300. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) & ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) ⇒ ⊢ (𝜑 → 𝐻:𝑌⟶𝐵) | ||
Theorem | cvmlift3lem4 35306* | Lemma for cvmlift2 35300. (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 35307* | Lemma for cvmlift2 35300. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ 𝐵 = ∪ 𝐶 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ SConn) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn) & ⊢ (𝜑 → 𝑂 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂)) & ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺) | ||
Theorem | cvmlift3lem6 35308* | Lemma for cvmlift3 35312. (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 35309* | Lemma for cvmlift3 35312. (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 35310* | Lemma for cvmlift2 35300. (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 35311* | Lemma for cvmlift2 35300. (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 35312* | A general version of cvmlift 35283. 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 35313* | The function 𝐹 from snmlval 35315 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 35314* | The function 𝐹 from snmlval 35315 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 35315* | 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 35316* | 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 35317 | The Godel-set of membership. |
class ∈𝑔 | ||
Syntax | cgna 35318 | The Godel-set for the Sheffer stroke. |
class ⊼𝑔 | ||
Syntax | cgol 35319 | The Godel-set of universal quantification. (Note that this is not a wff.) |
class ∀𝑔𝑁𝑈 | ||
Syntax | csat 35320 | The satisfaction function. |
class Sat | ||
Syntax | cfmla 35321 | The formula set predicate. |
class Fmla | ||
Syntax | csate 35322 | The ∈-satisfaction function. |
class Sat∈ | ||
Syntax | cprv 35323 | The "proves" relation. |
class ⊧ | ||
Definition | df-goel 35324 | 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 35325 | 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 35326 | 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 35327* |
Define the satisfaction predicate. This recursive construction builds up
a function over wff codes (see satff 35394) 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 35328* | 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 35329 | 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 35327 for the full coding scheme), see fmla0 35366, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 35370. 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 35428. (Fmla‘ω) = ∪ 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 35365. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛)) | ||
Definition | df-prv 35330* | 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 35414 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 35331 | 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 35332 | A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023.) |
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ (ω × (ω × ω))) | ||
Theorem | goeleq12bg 35333 | 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 35334 | The "Godel-set for the Sheffer stroke NAND" for two formulas 𝐴 and 𝐵. (Contributed by AV, 16-Oct-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴⊼𝑔𝐵) = 〈1o, 〈𝐴, 𝐵〉〉) | ||
Theorem | goaleq12d 35335 | Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023.) |
⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∀𝑔𝑀𝐴 = ∀𝑔𝑁𝐵) | ||
Theorem | gonanegoal 35336 | 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 35337* | 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 35338* | 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 35339 | 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 35340* | 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 35341* | 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 35342* | The value of the satisfaction predicate as function over wff codes at ∅. (Contributed by AV, 8-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}) | ||
Theorem | satfvsuclem1 35343* | Lemma 1 for satfvsuc 35345. (Contributed by AV, 8-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑m ω))} ∈ V) | ||
Theorem | satfvsuclem2 35344* | Lemma 2 for satfvsuc 35345. (Contributed by AV, 8-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ∈ V) | ||
Theorem | satfvsuc 35345* | 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 35346* | Lemma for satfv1 35347. (Contributed by AV, 9-Nov-2023.) |
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}) | ||
Theorem | satfv1 35347* | 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 35348 | 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 35349* | 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 35350* | 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 35351 | 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 35352* | Lemma for satfdm 35353. (Contributed by AV, 12-Oct-2023.) |
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st ‘𝑎)⊼𝑔(1st ‘𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑎)))) | ||
Theorem | satfdm 35353* | 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 35354 | 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 35355 | 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 35356* | 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 35357* | 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 35358* | 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 35359* | Lemma for satf0suc 35360, sat1el2xp 35363 and fmlasuc0 35368. (Contributed by AV, 19-Sep-2023.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑋 (∃𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃𝑤 ∈ 𝑍 𝑥 = 𝐶))} ∈ V) | ||
Theorem | satf0suc 35360* | 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 35361* | 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 35362 | 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 35363* | 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 35364 | 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 35365 | The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023.) |
⊢ (Fmla‘ω) = ∪ 𝑛 ∈ ω (Fmla‘𝑛) | ||
Theorem | fmla0 35366* | 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 35367 | 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 35368* | The valid Godel formulas of height (𝑁 + 1). (Contributed by AV, 18-Sep-2023.) |
⊢ (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))})) | ||
Theorem | fmlafvel 35369 | 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 35370* | 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 35371* | 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 35372* | The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023.) |
⊢ ((𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ (Fmla‘suc 𝑁) ↔ (𝐹 ∈ (Fmla‘𝑁) ∨ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝐹 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝐹 = ∀𝑔𝑖𝑢)))) | ||
Theorem | fmlasssuc 35373 | 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 35374 | The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.) |
⊢ (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁)) | ||
Theorem | fmlan0 35375 | The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023.) |
⊢ ∅ ∉ (Fmla‘ω) | ||
Theorem | gonan0 35376 | The "Godel-set of NAND" is a Godel formula of at least height 1. (Contributed by AV, 21-Oct-2023.) |
⊢ ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) | ||
Theorem | goaln0 35377* | The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023.) |
⊢ (∀𝑔𝑖𝐴 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) | ||
Theorem | gonarlem 35378* | Lemma for gonar 35379 (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 35379* | 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‘𝑁))) | ||
Theorem | goalrlem 35380* | Lemma for goalr 35381 (induction step). (Contributed by AV, 22-Oct-2023.) |
⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) | ||
Theorem | goalr 35381* | If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for 𝐴 being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023.) |
⊢ ((𝑁 ∈ ω ∧ ∀𝑔𝑖𝑎 ∈ (Fmla‘𝑁)) → 𝑎 ∈ (Fmla‘𝑁)) | ||
Theorem | fmla0disjsuc 35382* | The set of valid Godel formulas of height 0 is disjoint with the formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification. (Contributed by AV, 20-Oct-2023.) |
⊢ ((Fmla‘∅) ∩ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘∅)(∃𝑣 ∈ (Fmla‘∅)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) = ∅ | ||
Theorem | fmlasucdisj 35383* | The valid Godel formulas of height (𝑁 + 1) is disjoint with the difference ((Fmla‘suc suc 𝑁) ∖ (Fmla‘suc 𝑁)), expressed by formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification based on the valid Godel formulas of height (𝑁 + 1). (Contributed by AV, 20-Oct-2023.) |
⊢ (𝑁 ∈ ω → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑢 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑣 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ∨ ∃𝑢 ∈ (Fmla‘𝑁)∃𝑣 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑢⊼𝑔𝑣))}) = ∅) | ||
Theorem | satfdmfmla 35384 | The domain of the satisfaction predicate as function over wff codes in any model 𝑀 and any binary relation 𝐸 on 𝑀 for a natural number 𝑁 is the set of valid Godel formulas of height 𝑁. (Contributed by AV, 13-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁)) | ||
Theorem | satffunlem 35385 | Lemma for satffunlem1lem1 35386 and satffunlem2lem1 35388. (Contributed by AV, 27-Oct-2023.) |
⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤) | ||
Theorem | satffunlem1lem1 35386* | Lemma for satffunlem1 35391. (Contributed by AV, 17-Oct-2023.) |
⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → Fun {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) | ||
Theorem | satffunlem1lem2 35387* | Lemma 2 for satffunlem1 35391. (Contributed by AV, 23-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑗 ∈ 𝑀 ({〈𝑖, 𝑗〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) = ∅) | ||
Theorem | satffunlem2lem1 35388* | Lemma 1 for satffunlem2 35392. (Contributed by AV, 28-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) & ⊢ 𝐴 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) & ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⇒ ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → Fun {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = 𝐴))}) | ||
Theorem | dmopab3rexdif 35389* | The domain of an ordered pair class abstraction with three nested restricted existential quantifiers with differences. (Contributed by AV, 25-Oct-2023.) |
⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑥 = 𝐴)}) | ||
Theorem | satffunlem2lem2 35390* | Lemma 2 for satffunlem2 35392. (Contributed by AV, 27-Oct-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) & ⊢ 𝐴 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) & ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ⇒ ⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (dom (𝑆‘suc 𝑁) ∩ dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = 𝐴))}) = ∅) | ||
Theorem | satffunlem1 35391 | Lemma 1 for satffun 35393: induction basis. (Contributed by AV, 28-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘suc ∅)) | ||
Theorem | satffunlem2 35392 | Lemma 2 for satffun 35393: induction step. (Contributed by AV, 28-Oct-2023.) |
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁))) | ||
Theorem | satffun 35393 | The value of the satisfaction predicate as function over wff codes at a natural number is a function. (Contributed by AV, 28-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Fun ((𝑀 Sat 𝐸)‘𝑁)) | ||
Theorem | satff 35394 | The satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀. (Contributed by AV, 28-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → ((𝑀 Sat 𝐸)‘𝑁):(Fmla‘𝑁)⟶𝒫 (𝑀 ↑m ω)) | ||
Theorem | satfun 35395 | The satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀. (Contributed by AV, 29-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘ω):(Fmla‘ω)⟶𝒫 (𝑀 ↑m ω)) | ||
Theorem | satfvel 35396 | An element of the value of the satisfaction predicate as function over wff codes in the model 𝑀 and the binary relation 𝐸 on 𝑀 at the code 𝑈 for a wff using ∈ , ⊼ , ∀ is a valuation 𝑆:ω⟶𝑀 of the variables (v0 = (𝑆‘∅), v1 = (𝑆‘1o), etc.) so that 𝑈 is true under the assignment 𝑆. (Contributed by AV, 29-Oct-2023.) |
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (((𝑀 Sat 𝐸)‘ω)‘𝑈)) → 𝑆:ω⟶𝑀) | ||
Theorem | satfv0fvfmla0 35397* | The value of the satisfaction predicate as function over a wff code at ∅. (Contributed by AV, 2-Nov-2023.) |
⊢ 𝑆 = (𝑀 Sat 𝐸) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑋 ∈ (Fmla‘∅)) → ((𝑆‘∅)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st ‘(2nd ‘𝑋)))𝐸(𝑎‘(2nd ‘(2nd ‘𝑋)))}) | ||
Theorem | satefv 35398 | The simplified satisfaction predicate as function over wff codes in the model 𝑀 at the code 𝑈. (Contributed by AV, 30-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊) → (𝑀 Sat∈ 𝑈) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑈)) | ||
Theorem | sate0 35399 | The simplified satisfaction predicate for any wff code over an empty model. (Contributed by AV, 6-Oct-2023.) (Revised by AV, 5-Nov-2023.) |
⊢ (𝑈 ∈ 𝑉 → (∅ Sat∈ 𝑈) = (((∅ Sat ∅)‘ω)‘𝑈)) | ||
Theorem | satef 35400 | The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.) |
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (𝑀 Sat∈ 𝑈)) → 𝑆:ω⟶𝑀) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |