P. 357 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35601-35700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isfmlasuc 35601*	The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023.)
⊢ ((𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ (Fmla‘suc 𝑁) ↔ (𝐹 ∈ (Fmla‘𝑁) ∨ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝐹 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝐹 = ∀𝑔𝑖𝑢))))
Theorem	fmlasssuc 35602	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 35603	The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.)
⊢ (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁))
Theorem	fmlan0 35604	The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023.)
⊢ ∅ ∉ (Fmla‘ω)
Theorem	gonan0 35605	The "Godel-set of NAND" is a Godel formula of at least height 1. (Contributed by AV, 21-Oct-2023.)
⊢ ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅)
Theorem	goaln0 35606*	The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023.)
⊢ (∀𝑔𝑖𝐴 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅)
Theorem	gonarlem 35607*	Lemma for gonar 35608 (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 35608*	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 35609*	Lemma for goalr 35610 (induction step). (Contributed by AV, 22-Oct-2023.)
⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))))
Theorem	goalr 35610*	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 35611*	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 35612*	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 35613	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 35614	Lemma for satffunlem1lem1 35615 and satffunlem2lem1 35617. (Contributed by AV, 27-Oct-2023.)
⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤)
Theorem	satffunlem1lem1 35615*	Lemma for satffunlem1 35620. (Contributed by AV, 17-Oct-2023.)
⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → Fun {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
Theorem	satffunlem1lem2 35616*	Lemma 2 for satffunlem1 35620. (Contributed by AV, 23-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) = ∅)
Theorem	satffunlem2lem1 35617*	Lemma 1 for satffunlem2 35621. (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 35618*	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 35619*	Lemma 2 for satffunlem2 35621. (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 35620	Lemma 1 for satffun 35622: induction basis. (Contributed by AV, 28-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘suc ∅))
Theorem	satffunlem2 35621	Lemma 2 for satffun 35622: induction step. (Contributed by AV, 28-Oct-2023.)
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁)))
Theorem	satffun 35622	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 35623	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 35624	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 35625	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 35626*	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 35627	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 35628	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 35629	The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (𝑀 Sat∈ 𝑈)) → 𝑆:ω⟶𝑀)
Theorem	sate0fv0 35630	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 35631*	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 35632	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 35633	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 35634*	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 35635*	Instance of sategoelfv 35633 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 35636*	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 35637	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 35638*	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 35639*	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 35640	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 35641	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 35642	The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9528. (Contributed by AV, 5-Nov-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴)))
Theorem	prv0 35643	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 35644	No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023.)
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋 ∈ 𝑉) → ¬ {𝑋}⊧(𝐼∈𝑔𝐽))
21.6.11  Godel-sets of formulas - part 2
Syntax	cgon 35645	The Godel-set of negation. (Note that this is not a wff.)
class ¬𝑔𝑈
Syntax	cgoa 35646	The Godel-set of conjunction.
class ∧𝑔
Syntax	cgoi 35647	The Godel-set of implication.
class →𝑔
Syntax	cgoo 35648	The Godel-set of disjunction.
class ∨𝑔
Syntax	cgob 35649	The Godel-set of equivalence.
class ↔𝑔
Syntax	cgoq 35650	The Godel-set of equality.
class =𝑔
Syntax	cgox 35651	The Godel-set of existential quantification. (Note that this is not a wff.)
class ∃𝑔𝑁𝑈
Definition	df-gonot 35652	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 35653*	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 35654*	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 35655*	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 35656*	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 35657*	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 2709 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 35658	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.)
⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈
21.6.12  Models of ZF
Syntax	cgze 35659	The Axiom of Extensionality.
class AxExt
Syntax	cgzr 35660	The Axiom Scheme of Replacement.
class AxRep
Syntax	cgzp 35661	The Axiom of Power Sets.
class AxPow
Syntax	cgzu 35662	The Axiom of Unions.
class AxUn
Syntax	cgzg 35663	The Axiom of Regularity.
class AxReg
Syntax	cgzi 35664	The Axiom of Infinity.
class AxInf
Syntax	cgzf 35665	The set of models of ZF.
class ZF
Definition	df-gzext 35666	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 35667	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 35668	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 35669	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 35670	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 35671	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 35672*	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‘𝑢))}
21.6.13  Metamath formal systems 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 35673	The set of constants.
class mCN
Syntax	cmvar 35674	The set of variables.
class mVR
Syntax	cmty 35675	The type function.
class mType
Syntax	cmvt 35676	The set of variable typecodes.
class mVT
Syntax	cmtc 35677	The set of typecodes.
class mTC
Syntax	cmax 35678	The set of axioms.
class mAx
Syntax	cmrex 35679	The set of raw expressions.
class mREx
Syntax	cmex 35680	The set of expressions.
class mEx
Syntax	cmdv 35681	The set of distinct variables.
class mDV
Syntax	cmvrs 35682	The variables in an expression.
class mVars
Syntax	cmrsub 35683	The set of raw substitutions.
class mRSubst
Syntax	cmsub 35684	The set of substitutions.
class mSubst
Syntax	cmvh 35685	The set of variable hypotheses.
class mVH
Syntax	cmpst 35686	The set of pre-statements.
class mPreSt
Syntax	cmsr 35687	The reduct of a pre-statement.
class mStRed
Syntax	cmsta 35688	The set of statements.
class mStat
Syntax	cmfs 35689	The set of formal systems.
class mFS
Syntax	cmcls 35690	The closure of a set of statements.
class mCls
Syntax	cmpps 35691	The set of provable pre-statements.
class mPPSt
Syntax	cmthm 35692	The set of theorems.
class mThm
Definition	df-mcn 35693	Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mCN = Slot 1
Definition	df-mvar 35694	Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVR = Slot 2
Definition	df-mty 35695	Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mType = Slot 3
Definition	df-mtc 35696	Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTC = Slot 4
Definition	df-mmax 35697	Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mAx = Slot 5
Definition	df-mvt 35698	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 35699	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 35700	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‘𝑡)))