| Metamath
Proof Explorer Theorem List (p. 355 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 | goalrlem 35401* | Lemma for goalr 35402 (induction step). (Contributed by AV, 22-Oct-2023.) |
| ⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁)))) | ||
| Theorem | goalr 35402* | 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 35403* | 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 35404* | 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 35405 | 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 35406 | Lemma for satffunlem1lem1 35407 and satffunlem2lem1 35409. (Contributed by AV, 27-Oct-2023.) |
| ⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤) | ||
| Theorem | satffunlem1lem1 35407* | Lemma for satffunlem1 35412. (Contributed by AV, 17-Oct-2023.) |
| ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → Fun {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) | ||
| Theorem | satffunlem1lem2 35408* | Lemma 2 for satffunlem1 35412. (Contributed by AV, 23-Oct-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑗 ∈ 𝑀 ({〈𝑖, 𝑗〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) = ∅) | ||
| Theorem | satffunlem2lem1 35409* | Lemma 1 for satffunlem2 35413. (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 35410* | 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 35411* | Lemma 2 for satffunlem2 35413. (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 35412 | Lemma 1 for satffun 35414: induction basis. (Contributed by AV, 28-Oct-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘suc ∅)) | ||
| Theorem | satffunlem2 35413 | Lemma 2 for satffun 35414: induction step. (Contributed by AV, 28-Oct-2023.) |
| ⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁))) | ||
| Theorem | satffun 35414 | 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 35415 | 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 35416 | 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 35417 | 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 35418* | 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 35419 | 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 35420 | 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 35421 | The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (𝑀 Sat∈ 𝑈)) → 𝑆:ω⟶𝑀) | ||
| Theorem | sate0fv0 35422 | A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023.) |
| ⊢ (𝑈 ∈ (Fmla‘ω) → (𝑆 ∈ (∅ Sat∈ 𝑈) → 𝑆 = ∅)) | ||
| Theorem | satefvfmla0 35423* | The simplified satisfaction predicate for wff codes of height 0. (Contributed by AV, 4-Nov-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑋 ∈ (Fmla‘∅)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘(1st ‘(2nd ‘𝑋))) ∈ (𝑎‘(2nd ‘(2nd ‘𝑋)))}) | ||
| Theorem | sategoelfvb 35424 | Characterization of a valuation 𝑆 of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
| ⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝑆 ∈ 𝐸 ↔ (𝑆 ∈ (𝑀 ↑m ω) ∧ (𝑆‘𝐴) ∈ (𝑆‘𝐵)))) | ||
| Theorem | sategoelfv 35425 | Condition of a valuation 𝑆 of a simplified satisfaction predicate for a Godel-set of membership: The sets in model 𝑀 corresponding to the variables 𝐴 and 𝐵 under the assignment of 𝑆 are in a membership relation in 𝑀. (Contributed by AV, 5-Nov-2023.) |
| ⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑆 ∈ 𝐸) → (𝑆‘𝐴) ∈ (𝑆‘𝐵)) | ||
| Theorem | ex-sategoelel 35426* | Example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
| ⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) & ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 𝐴, 𝑍, if(𝑥 = 𝐵, 𝒫 𝑍, ∅))) ⇒ ⊢ (((𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵)) → 𝑆 ∈ 𝐸) | ||
| Theorem | ex-sategoel 35427* | Instance of sategoelfv 35425 for the example of a valuation of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023.) |
| ⊢ 𝐸 = (𝑀 Sat∈ (𝐴∈𝑔𝐵)) & ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 𝐴, 𝑍, if(𝑥 = 𝐵, 𝒫 𝑍, ∅))) ⇒ ⊢ (((𝑀 ∈ WUni ∧ 𝑍 ∈ 𝑀) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ≠ 𝐵)) → (𝑆‘𝐴) ∈ (𝑆‘𝐵)) | ||
| Theorem | satfv1fvfmla1 35428* | The value of the satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.) |
| ⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ⇒ ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat 𝐸)‘1o)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) | ||
| Theorem | 2goelgoanfmla1 35429 | Two Godel-sets of membership combined with a Godel-set for NAND is a Godel formula of height 1. (Contributed by AV, 17-Nov-2023.) |
| ⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ⇒ ⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ (Fmla‘1o)) | ||
| Theorem | satefvfmla1 35430* | The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.) |
| ⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 Sat∈ 𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬ (𝑎‘𝐼) ∈ (𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾) ∈ (𝑎‘𝐿))}) | ||
| Theorem | ex-sategoelelomsuc 35431* | Example of a valuation of a simplified satisfaction predicate over the ordinal numbers as model for a Godel-set of membership using the properties of a successor: (𝑆‘2o) = 𝑍 ∈ suc 𝑍 = (𝑆‘2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2o∈𝑔1o) should not be confused with 2o ∈ 1o, which is false. (Contributed by AV, 19-Nov-2023.) |
| ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 2o, 𝑍, suc 𝑍)) ⇒ ⊢ (𝑍 ∈ ω → 𝑆 ∈ (ω Sat∈ (2o∈𝑔1o))) | ||
| Theorem | ex-sategoelel12 35432 | Example of a valuation of a simplified satisfaction predicate over a proper pair (of ordinal numbers) as model for a Godel-set of membership using the properties of a successor: (𝑆‘2o) = 1o ∈ 2o = (𝑆‘2o). Remark: the indices 1o and 2o are intentionally reversed to distinguish them from elements of the model: (2o∈𝑔1o) should not be confused with 2o ∈ 1o, which is false. (Contributed by AV, 19-Nov-2023.) |
| ⊢ 𝑆 = (𝑥 ∈ ω ↦ if(𝑥 = 2o, 1o, 2o)) ⇒ ⊢ 𝑆 ∈ ({1o, 2o} Sat∈ (2o∈𝑔1o)) | ||
| Theorem | prv 35433 | The "proves" relation on a set. A wff encoded as 𝑈 is true in a model 𝑀 iff for every valuation 𝑠 ∈ (𝑀 ↑m ω), the interpretation of the wff using the membership relation on 𝑀 is true. (Contributed by AV, 5-Nov-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ 𝑊) → (𝑀⊧𝑈 ↔ (𝑀 Sat∈ 𝑈) = (𝑀 ↑m ω))) | ||
| Theorem | elnanelprv 35434 | The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9647. (Contributed by AV, 5-Nov-2023.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴))) | ||
| Theorem | prv0 35435 | Every wff encoded as 𝑈 is true in an "empty model" (𝑀 = ∅). 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, because ∃𝑥𝑥 = 𝑥 is not satisfied on the empty model. (Contributed by AV, 19-Nov-2023.) |
| ⊢ (𝑈 ∈ (Fmla‘ω) → ∅⊧𝑈) | ||
| Theorem | prv1n 35436 | No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023.) |
| ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽)) | ||
| Syntax | cgon 35437 | The Godel-set of negation. (Note that this is not a wff.) |
| class ¬𝑔𝑈 | ||
| Syntax | cgoa 35438 | The Godel-set of conjunction. |
| class ∧𝑔 | ||
| Syntax | cgoi 35439 | The Godel-set of implication. |
| class →𝑔 | ||
| Syntax | cgoo 35440 | The Godel-set of disjunction. |
| class ∨𝑔 | ||
| Syntax | cgob 35441 | The Godel-set of equivalence. |
| class ↔𝑔 | ||
| Syntax | cgoq 35442 | The Godel-set of equality. |
| class =𝑔 | ||
| Syntax | cgox 35443 | The Godel-set of existential quantification. (Note that this is not a wff.) |
| class ∃𝑔𝑁𝑈 | ||
| Definition | df-gonot 35444 | Define the Godel-set of negation. Here the argument 𝑈 is also a Godel-set corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ ¬𝑔𝑈 = (𝑈⊼𝑔𝑈) | ||
| Definition | df-goan 35445* | Define the Godel-set of conjunction. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ ∧𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ ¬𝑔(𝑢⊼𝑔𝑣)) | ||
| Definition | df-goim 35446* | Define the Godel-set of implication. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ →𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢⊼𝑔¬𝑔𝑣)) | ||
| Definition | df-goor 35447* | Define the Godel-set of disjunction. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ ∨𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ (¬𝑔𝑢 →𝑔 𝑣)) | ||
| Definition | df-gobi 35448* | Define the Godel-set of equivalence. Here the arguments 𝑈 and 𝑉 are also Godel-sets corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ ↔𝑔 = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑢 →𝑔 𝑣)∧𝑔(𝑣 →𝑔 𝑢))) | ||
| Definition | df-goeq 35449* | Define the Godel-set of equality. Here the arguments 𝑥 = 〈𝑁, 𝑃〉 correspond to vN and vP , so (∅=𝑔1o) actually means v0 = v1 , not 0 = 1. Here we use the trick mentioned in ax-ext 2708 to introduce equality as a defined notion in terms of ∈𝑔. The expression suc (𝑢 ∪ 𝑣) = max (𝑢, 𝑣) + 1 here is a convenient way of getting a dummy variable distinct from 𝑢 and 𝑣. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ =𝑔 = (𝑢 ∈ ω, 𝑣 ∈ ω ↦ ⦋suc (𝑢 ∪ 𝑣) / 𝑤⦌∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣))) | ||
| Definition | df-goex 35450 | Define the Godel-set of existential 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.) |
| ⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈 | ||
| Syntax | cgze 35451 | The Axiom of Extensionality. |
| class AxExt | ||
| Syntax | cgzr 35452 | The Axiom Scheme of Replacement. |
| class AxRep | ||
| Syntax | cgzp 35453 | The Axiom of Power Sets. |
| class AxPow | ||
| Syntax | cgzu 35454 | The Axiom of Unions. |
| class AxUn | ||
| Syntax | cgzg 35455 | The Axiom of Regularity. |
| class AxReg | ||
| Syntax | cgzi 35456 | The Axiom of Infinity. |
| class AxInf | ||
| Syntax | cgzf 35457 | The set of models of ZF. |
| class ZF | ||
| Definition | df-gzext 35458 | The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ AxExt = (∀𝑔2o((2o∈𝑔∅) ↔𝑔 (2o∈𝑔1o)) →𝑔 (∅=𝑔1o)) | ||
| Definition | df-gzrep 35459 | The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ AxRep = (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o)) →𝑔 ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)))) | ||
| Definition | df-gzpow 35460 | The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ AxPow = ∃𝑔1o∀𝑔2o(∀𝑔1o((1o∈𝑔2o) ↔𝑔 (1o∈𝑔∅)) →𝑔 (2o∈𝑔1o)) | ||
| Definition | df-gzun 35461 | The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ AxUn = ∃𝑔1o∀𝑔2o(∃𝑔1o((2o∈𝑔1o)∧𝑔(1o∈𝑔∅)) →𝑔 (2o∈𝑔1o)) | ||
| Definition | df-gzreg 35462 | The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ AxReg = (∃𝑔1o(1o∈𝑔∅) →𝑔 ∃𝑔1o((1o∈𝑔∅)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅)))) | ||
| Definition | df-gzinf 35463 | The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ AxInf = ∃𝑔1o((∅∈𝑔1o)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o)))) | ||
| Definition | df-gzf 35464* | Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| ⊢ ZF = {𝑚 ∣ ((Tr 𝑚 ∧ 𝑚⊧AxExt ∧ 𝑚⊧AxPow) ∧ (𝑚⊧AxUn ∧ 𝑚⊧AxReg ∧ 𝑚⊧AxInf) ∧ ∀𝑢 ∈ (Fmla‘ω)𝑚⊧(AxRep‘𝑢))} | ||
This is a formalization of Appendix C of the Metamath book, which describes the mathematical representation of a formal system, of which set.mm (this file) is one. | ||
| Syntax | cmcn 35465 | The set of constants. |
| class mCN | ||
| Syntax | cmvar 35466 | The set of variables. |
| class mVR | ||
| Syntax | cmty 35467 | The type function. |
| class mType | ||
| Syntax | cmvt 35468 | The set of variable typecodes. |
| class mVT | ||
| Syntax | cmtc 35469 | The set of typecodes. |
| class mTC | ||
| Syntax | cmax 35470 | The set of axioms. |
| class mAx | ||
| Syntax | cmrex 35471 | The set of raw expressions. |
| class mREx | ||
| Syntax | cmex 35472 | The set of expressions. |
| class mEx | ||
| Syntax | cmdv 35473 | The set of distinct variables. |
| class mDV | ||
| Syntax | cmvrs 35474 | The variables in an expression. |
| class mVars | ||
| Syntax | cmrsub 35475 | The set of raw substitutions. |
| class mRSubst | ||
| Syntax | cmsub 35476 | The set of substitutions. |
| class mSubst | ||
| Syntax | cmvh 35477 | The set of variable hypotheses. |
| class mVH | ||
| Syntax | cmpst 35478 | The set of pre-statements. |
| class mPreSt | ||
| Syntax | cmsr 35479 | The reduct of a pre-statement. |
| class mStRed | ||
| Syntax | cmsta 35480 | The set of statements. |
| class mStat | ||
| Syntax | cmfs 35481 | The set of formal systems. |
| class mFS | ||
| Syntax | cmcls 35482 | The closure of a set of statements. |
| class mCls | ||
| Syntax | cmpps 35483 | The set of provable pre-statements. |
| class mPPSt | ||
| Syntax | cmthm 35484 | The set of theorems. |
| class mThm | ||
| Definition | df-mcn 35485 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mCN = Slot 1 | ||
| Definition | df-mvar 35486 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mVR = Slot 2 | ||
| Definition | df-mty 35487 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mType = Slot 3 | ||
| Definition | df-mtc 35488 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mTC = Slot 4 | ||
| Definition | df-mmax 35489 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mAx = Slot 5 | ||
| Definition | df-mvt 35490 | Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mVT = (𝑡 ∈ V ↦ ran (mType‘𝑡)) | ||
| Definition | df-mrex 35491 | Define the set of "raw expressions", which are expressions without a typecode attached. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mREx = (𝑡 ∈ V ↦ Word ((mCN‘𝑡) ∪ (mVR‘𝑡))) | ||
| Definition | df-mex 35492 | Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mEx = (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡))) | ||
| Definition | df-mdv 35493 | Define the set of distinct variable conditions, which are pairs of distinct variables. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mDV = (𝑡 ∈ V ↦ (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I )) | ||
| Definition | df-mvrs 35494* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡)))) | ||
| Definition | df-mrsub 35495* | Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mRSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mREx‘𝑡) ↦ ((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) | ||
| Definition | df-msub 35496* | Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd ‘𝑒))〉))) | ||
| Definition | df-mvh 35497* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mVH = (𝑡 ∈ V ↦ (𝑣 ∈ (mVR‘𝑡) ↦ 〈((mType‘𝑡)‘𝑣), 〈“𝑣”〉〉)) | ||
| Definition | df-mpst 35498* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))) | ||
| Definition | df-msr 35499* | Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd ‘𝑠) / 𝑎⦌〈((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | ||
| Definition | df-msta 35500 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
| ⊢ mStat = (𝑡 ∈ V ↦ ran (mStRed‘𝑡)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |