Definition df-sat 36087

Description: Define the satisfaction predicate. This recursive construction builds up a function over wff codes (see satff 36154) 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 (v₀ = (𝑆‘∅), v₁ = (𝑆‘1_o), 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

• v_i ∈ v_j is coded as ⟨∅, ⟨𝑖, 𝑗⟩⟩,
• (𝜑 ⊼ 𝜓) is coded as ⟨1_o, ⟨𝜑, 𝜓⟩⟩, and
• ∀ v_i 𝜑 is coded as ⟨2_o, ⟨𝑖, 𝜑⟩⟩.

(Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-sat	⊢ Sat = (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω))

Distinct variable group:   𝑒,𝑎,𝑓,𝑖,𝑗,𝑚,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-sat

Step	Hyp	Ref	Expression
1		csat 36080	. 2 class Sat
2		vm	. . 3 setvar 𝑚
3		ve	. . 3 setvar 𝑒
4		cvv 3451	. . 3 class V
5		vf	. . . . . 6 setvar 𝑓
6	5	cv 1569	. . . . . . 7 class 𝑓
7		vx	. . . . . . . . . . . . . 14 setvar 𝑥
8	7	cv 1569	. . . . . . . . . . . . 13 class 𝑥
9		vu	. . . . . . . . . . . . . . . 16 setvar 𝑢
10	9	cv 1569	. . . . . . . . . . . . . . 15 class 𝑢
11		c1st 7997	. . . . . . . . . . . . . . 15 class 1st
12	10, 11	cfv 6537	. . . . . . . . . . . . . 14 class (1st ‘𝑢)
13		vv	. . . . . . . . . . . . . . . 16 setvar 𝑣
14	13	cv 1569	. . . . . . . . . . . . . . 15 class 𝑣
15	14, 11	cfv 6537	. . . . . . . . . . . . . 14 class (1st ‘𝑣)
16		cgna 36078	. . . . . . . . . . . . . 14 class ⊼𝑔
17	12, 15, 16	co 7418	. . . . . . . . . . . . 13 class ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))
18	8, 17	wceq 1570	. . . . . . . . . . . 12 wff 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))
19		vy	. . . . . . . . . . . . . 14 setvar 𝑦
20	19	cv 1569	. . . . . . . . . . . . 13 class 𝑦
21	2	cv 1569	. . . . . . . . . . . . . . 15 class 𝑚
22		com 7875	. . . . . . . . . . . . . . 15 class ω
23		cmap 8840	. . . . . . . . . . . . . . 15 class ↑m
24	21, 22, 23	co 7418	. . . . . . . . . . . . . 14 class (𝑚 ↑m ω)
25		c2nd 7998	. . . . . . . . . . . . . . . 16 class 2nd
26	10, 25	cfv 6537	. . . . . . . . . . . . . . 15 class (2nd ‘𝑢)
27	14, 25	cfv 6537	. . . . . . . . . . . . . . 15 class (2nd ‘𝑣)
28	26, 27	cin 3898	. . . . . . . . . . . . . 14 class ((2nd ‘𝑢) ∩ (2nd ‘𝑣))
29	24, 28	cdif 3896	. . . . . . . . . . . . 13 class ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))
30	20, 29	wceq 1570	. . . . . . . . . . . 12 wff 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))
31	18, 30	wa 401	. . . . . . . . . . 11 wff (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))
32	31, 13, 6	wrex 3087	. . . . . . . . . 10 wff ∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))
33		vi	. . . . . . . . . . . . . . 15 setvar 𝑖
34	33	cv 1569	. . . . . . . . . . . . . 14 class 𝑖
35	12, 34	cgol 36079	. . . . . . . . . . . . 13 class ∀𝑔𝑖(1st ‘𝑢)
36	8, 35	wceq 1570	. . . . . . . . . . . 12 wff 𝑥 = ∀𝑔𝑖(1st ‘𝑢)
37		vz	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑧
38	37	cv 1569	. . . . . . . . . . . . . . . . . . 19 class 𝑧
39	34, 38	cop 4590	. . . . . . . . . . . . . . . . . 18 class ⟨𝑖, 𝑧⟩
40	39	csn 4584	. . . . . . . . . . . . . . . . 17 class {⟨𝑖, 𝑧⟩}
41		va	. . . . . . . . . . . . . . . . . . 19 setvar 𝑎
42	41	cv 1569	. . . . . . . . . . . . . . . . . 18 class 𝑎
43	34	csn 4584	. . . . . . . . . . . . . . . . . . 19 class {𝑖}
44	22, 43	cdif 3896	. . . . . . . . . . . . . . . . . 18 class (ω ∖ {𝑖})
45	42, 44	cres 5653	. . . . . . . . . . . . . . . . 17 class (𝑎 ↾ (ω ∖ {𝑖}))
46	40, 45	cun 3897	. . . . . . . . . . . . . . . 16 class ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖})))
47	46, 26	wcel 2145	. . . . . . . . . . . . . . 15 wff ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)
48	47, 37, 21	wral 3077	. . . . . . . . . . . . . 14 wff ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)
49	48, 41, 24	crab 3413	. . . . . . . . . . . . 13 class {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}
50	20, 49	wceq 1570	. . . . . . . . . . . 12 wff 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}
51	36, 50	wa 401	. . . . . . . . . . 11 wff (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})
52	51, 33, 22	wrex 3087	. . . . . . . . . 10 wff ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})
53	32, 52	wo 861	. . . . . . . . 9 wff (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
54	53, 9, 6	wrex 3087	. . . . . . . 8 wff ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
55	54, 7, 19	copab 5167	. . . . . . 7 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}
56	6, 55	cun 3897	. . . . . 6 class (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
57	5, 4, 56	cmpt 5186	. . . . 5 class (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
58		vj	. . . . . . . . . . . 12 setvar 𝑗
59	58	cv 1569	. . . . . . . . . . 11 class 𝑗
60		cgoe 36077	. . . . . . . . . . 11 class ∈𝑔
61	34, 59, 60	co 7418	. . . . . . . . . 10 class (𝑖∈𝑔𝑗)
62	8, 61	wceq 1570	. . . . . . . . 9 wff 𝑥 = (𝑖∈𝑔𝑗)
63	34, 42	cfv 6537	. . . . . . . . . . . 12 class (𝑎‘𝑖)
64	59, 42	cfv 6537	. . . . . . . . . . . 12 class (𝑎‘𝑗)
65	3	cv 1569	. . . . . . . . . . . 12 class 𝑒
66	63, 64, 65	wbr 5103	. . . . . . . . . . 11 wff (𝑎‘𝑖)𝑒(𝑎‘𝑗)
67	66, 41, 24	crab 3413	. . . . . . . . . 10 class {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}
68	20, 67	wceq 1570	. . . . . . . . 9 wff 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}
69	62, 68	wa 401	. . . . . . . 8 wff (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})
70	69, 58, 22	wrex 3087	. . . . . . 7 wff ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})
71	70, 33, 22	wrex 3087	. . . . . 6 wff ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})
72	71, 7, 19	copab 5167	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}
73	57, 72	crdg 8410	. . . 4 class rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})})
74	22	csuc 6363	. . . 4 class suc ω
75	73, 74	cres 5653	. . 3 class (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω)
76	2, 3, 4, 4, 75	cmpo 7420	. 2 class (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω))
77	1, 76	wceq 1570	1 wff Sat = (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω))

This definition is used by:  satf  36097