P. 358 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35701-35800   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	csate 35701	The ∈-satisfaction function.
class Sat∈
Syntax	cprv 35702	The "proves" relation.
class ⊧
Definition	df-goel 35703	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 35704	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 35705	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 35706*	Define the satisfaction predicate. This recursive construction builds up a function over wff codes (see satff 35773) 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 vi ∈ vj is coded as ⟨∅, ⟨𝑖, 𝑗⟩⟩, (𝜑 ⊼ 𝜓) is coded as ⟨1o, ⟨𝜑, 𝜓⟩⟩, and ∀ vi 𝜑 is coded as ⟨2o, ⟨𝑖, 𝜑⟩⟩. (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 35707*	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 35708	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 35706 for the full coding scheme), see fmla0 35745, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 35749. 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 35807. (Fmla‘ω) = ∪ 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 35744. (Contributed by Mario Carneiro, 14-Jul-2013.)
⊢ Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))
Definition	df-prv 35709*	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 35793 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 35710	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 35711	A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023.)
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝐼∈𝑔𝐽) ∈ (ω × (ω × ω)))
Theorem	goeleq12bg 35712	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 35713	The "Godel-set for the Sheffer stroke NAND" for two formulas 𝐴 and 𝐵. (Contributed by AV, 16-Oct-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴⊼𝑔𝐵) = ⟨1o, ⟨𝐴, 𝐵⟩⟩)
Theorem	goaleq12d 35714	Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∀𝑔𝑀𝐴 = ∀𝑔𝑁𝐵)
Theorem	gonanegoal 35715	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 35716*	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 35717*	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 35718	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 35719*	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 35720*	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 35721*	The value of the satisfaction predicate as function over wff codes at ∅. (Contributed by AV, 8-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
Theorem	satfvsuclem1 35722*	Lemma 1 for satfvsuc 35724. (Contributed by AV, 8-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑m ω))} ∈ V)
Theorem	satfvsuclem2 35723*	Lemma 2 for satfvsuc 35724. (Contributed by AV, 8-Oct-2023.)
⊢ 𝑆 = (𝑀 Sat 𝐸)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ∈ V)
Theorem	satfvsuc 35724*	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 35725*	Lemma for satfv1 35726. (Contributed by AV, 9-Nov-2023.)
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑁, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))})
Theorem	satfv1 35726*	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 35727	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 35728*	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 35729*	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 35730	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 35731*	Lemma for satfdm 35732. (Contributed by AV, 12-Oct-2023.)
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω) ∧ dom ((𝑀 Sat 𝐸)‘𝑌) = dom ((𝑁 Sat 𝐹)‘𝑌)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑌)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑌)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ∃𝑎 ∈ ((𝑁 Sat 𝐹)‘𝑌)(∃𝑏 ∈ ((𝑁 Sat 𝐹)‘𝑌)𝑥 = ((1st ‘𝑎)⊼𝑔(1st ‘𝑏)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑎))))
Theorem	satfdm 35732*	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 35733	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 35734	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 35735*	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 35736*	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 35737*	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 35738*	Lemma for satf0suc 35739, sat1el2xp 35742 and fmlasuc0 35747. (Contributed by AV, 19-Sep-2023.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑋 (∃𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃𝑤 ∈ 𝑍 𝑥 = 𝐶))} ∈ V)
Theorem	satf0suc 35739*	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 35740*	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 35741	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 35742*	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 35743	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 35744	The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023.)
⊢ (Fmla‘ω) = ∪ 𝑛 ∈ ω (Fmla‘𝑛)
Theorem	fmla0 35745*	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 35746	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 35747*	The valid Godel formulas of height (𝑁 + 1). (Contributed by AV, 18-Sep-2023.)
⊢ (𝑁 ∈ ω → (Fmla‘suc 𝑁) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))}))
Theorem	fmlafvel 35748	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 35749*	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 35750*	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 35751*	The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023.)
⊢ ((𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ (Fmla‘suc 𝑁) ↔ (𝐹 ∈ (Fmla‘𝑁) ∨ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝐹 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝐹 = ∀𝑔𝑖𝑢))))
Theorem	fmlasssuc 35752	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 35753	The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023.)
⊢ (𝑁 ∈ ω → ∅ ∉ (Fmla‘𝑁))
Theorem	fmlan0 35754	The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023.)
⊢ ∅ ∉ (Fmla‘ω)
Theorem	gonan0 35755	The "Godel-set of NAND" is a Godel formula of at least height 1. (Contributed by AV, 21-Oct-2023.)
⊢ ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅)
Theorem	goaln0 35756*	The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023.)
⊢ (∀𝑔𝑖𝐴 ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅)
Theorem	gonarlem 35757*	Lemma for gonar 35758 (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 35758*	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 35759*	Lemma for goalr 35760 (induction step). (Contributed by AV, 22-Oct-2023.)
⊢ (𝑁 ∈ ω → ((∀𝑔𝑖𝑎 ∈ (Fmla‘suc 𝑁) → 𝑎 ∈ (Fmla‘suc 𝑁)) → (∀𝑔𝑖𝑎 ∈ (Fmla‘suc suc 𝑁) → 𝑎 ∈ (Fmla‘suc suc 𝑁))))
Theorem	goalr 35760*	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 35761*	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 35762*	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 35763	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 35764	Lemma for satffunlem1lem1 35765 and satffunlem2lem1 35767. (Contributed by AV, 27-Oct-2023.)
⊢ (((Fun 𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤)
Theorem	satffunlem1lem1 35765*	Lemma for satffunlem1 35770. (Contributed by AV, 17-Oct-2023.)
⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → Fun {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
Theorem	satffunlem1lem2 35766*	Lemma 2 for satffunlem1 35770. (Contributed by AV, 23-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ((𝑀 Sat 𝐸)‘∅) ∩ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘∅)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘∅)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣ ∀𝑗 ∈ 𝑀 ({⟨𝑖, 𝑗⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) = ∅)
Theorem	satffunlem2lem1 35767*	Lemma 1 for satffunlem2 35771. (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 35768*	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 35769*	Lemma 2 for satffunlem2 35771. (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 35770	Lemma 1 for satffun 35772: induction basis. (Contributed by AV, 28-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → Fun ((𝑀 Sat 𝐸)‘suc ∅))
Theorem	satffunlem2 35771	Lemma 2 for satffun 35772: induction step. (Contributed by AV, 28-Oct-2023.)
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc suc 𝑁)))
Theorem	satffun 35772	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 35773	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 35774	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 35775	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 35776*	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 35777	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 35778	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 35779	The simplified satisfaction predicate as function over wff codes over an empty model. (Contributed by AV, 30-Oct-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑈 ∈ (Fmla‘ω) ∧ 𝑆 ∈ (𝑀 Sat∈ 𝑈)) → 𝑆:ω⟶𝑀)
Theorem	sate0fv0 35780	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 35781*	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 35782	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 35783	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 35784*	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 35785*	Instance of sategoelfv 35783 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 35786*	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 35787	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 35788*	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 35789*	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 35790	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 35791	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 35792	The wff (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) encoded as ((𝐴∈𝑔𝐵) ⊼𝑔(𝐵∈𝑔𝐴)) is true in any model 𝑀. This is the model theoretic proof of elnanel 9564. (Contributed by AV, 5-Nov-2023.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝑀⊧((𝐴∈𝑔𝐵)⊼𝑔(𝐵∈𝑔𝐴)))
Theorem	prv0 35793	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 35794	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 35795	The Godel-set of negation. (Note that this is not a wff.)
class ¬𝑔𝑈
Syntax	cgoa 35796	The Godel-set of conjunction.
class ∧𝑔
Syntax	cgoi 35797	The Godel-set of implication.
class →𝑔
Syntax	cgoo 35798	The Godel-set of disjunction.
class ∨𝑔
Syntax	cgob 35799	The Godel-set of equivalence.
class ↔𝑔
Syntax	cgoq 35800	The Godel-set of equality.
class =𝑔