Definition df-sat 31325

Description: Define the satisfaction predicate. This recursive construction builds up a function over wff codes 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_𝑜), 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_𝑜, ⟨𝜑, 𝜓⟩⟩, and
• ∀ v_i 𝜑 is coded as ⟨2_𝑜, ⟨𝑖, 𝜑⟩⟩.

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

Assertion

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

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

Detailed syntax breakdown of Definition df-sat

Step	Hyp	Ref	Expression
1		csat 31318	. 2 class Sat
2		vm	. . 3 setvar 𝑚
3		ve	. . 3 setvar 𝑒
4		cvv 3200	. . 3 class V
5		vf	. . . . . 6 setvar 𝑓
6	5	cv 1482	. . . . . . 7 class 𝑓
7		vx	. . . . . . . . . . . . . 14 setvar 𝑥
8	7	cv 1482	. . . . . . . . . . . . 13 class 𝑥
9		vu	. . . . . . . . . . . . . . . 16 setvar 𝑢
10	9	cv 1482	. . . . . . . . . . . . . . 15 class 𝑢
11		c1st 7166	. . . . . . . . . . . . . . 15 class 1st
12	10, 11	cfv 5888	. . . . . . . . . . . . . 14 class (1st ‘𝑢)
13		vv	. . . . . . . . . . . . . . . 16 setvar 𝑣
14	13	cv 1482	. . . . . . . . . . . . . . 15 class 𝑣
15	14, 11	cfv 5888	. . . . . . . . . . . . . 14 class (1st ‘𝑣)
16		cgna 31316	. . . . . . . . . . . . . 14 class ⊼𝑔
17	12, 15, 16	co 6650	. . . . . . . . . . . . 13 class ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))
18	8, 17	wceq 1483	. . . . . . . . . . . 12 wff 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))
19		vy	. . . . . . . . . . . . . 14 setvar 𝑦
20	19	cv 1482	. . . . . . . . . . . . 13 class 𝑦
21	2	cv 1482	. . . . . . . . . . . . . . 15 class 𝑚
22		com 7065	. . . . . . . . . . . . . . 15 class ω
23		cmap 7857	. . . . . . . . . . . . . . 15 class ↑𝑚
24	21, 22, 23	co 6650	. . . . . . . . . . . . . 14 class (𝑚 ↑𝑚 ω)
25		c2nd 7167	. . . . . . . . . . . . . . . 16 class 2nd
26	10, 25	cfv 5888	. . . . . . . . . . . . . . 15 class (2nd ‘𝑢)
27	14, 25	cfv 5888	. . . . . . . . . . . . . . 15 class (2nd ‘𝑣)
28	26, 27	cin 3573	. . . . . . . . . . . . . 14 class ((2nd ‘𝑢) ∩ (2nd ‘𝑣))
29	24, 28	cdif 3571	. . . . . . . . . . . . 13 class ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))
30	20, 29	wceq 1483	. . . . . . . . . . . 12 wff 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))
31	18, 30	wa 384	. . . . . . . . . . 11 wff (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))
32	31, 13, 6	wrex 2913	. . . . . . . . . 10 wff ∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))))
33		vi	. . . . . . . . . . . . . . 15 setvar 𝑖
34	33	cv 1482	. . . . . . . . . . . . . 14 class 𝑖
35	12, 34	cgol 31317	. . . . . . . . . . . . 13 class ∀𝑔𝑖(1st ‘𝑢)
36	8, 35	wceq 1483	. . . . . . . . . . . 12 wff 𝑥 = ∀𝑔𝑖(1st ‘𝑢)
37		vz	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑧
38	37	cv 1482	. . . . . . . . . . . . . . . . . . 19 class 𝑧
39	34, 38	cop 4183	. . . . . . . . . . . . . . . . . 18 class ⟨𝑖, 𝑧⟩
40	39	csn 4177	. . . . . . . . . . . . . . . . 17 class {⟨𝑖, 𝑧⟩}
41		va	. . . . . . . . . . . . . . . . . . 19 setvar 𝑎
42	41	cv 1482	. . . . . . . . . . . . . . . . . 18 class 𝑎
43	34	csn 4177	. . . . . . . . . . . . . . . . . . 19 class {𝑖}
44	22, 43	cdif 3571	. . . . . . . . . . . . . . . . . 18 class (ω ∖ {𝑖})
45	42, 44	cres 5116	. . . . . . . . . . . . . . . . 17 class (𝑎 ↾ (ω ∖ {𝑖}))
46	40, 45	cun 3572	. . . . . . . . . . . . . . . 16 class ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖})))
47	46, 26	wcel 1990	. . . . . . . . . . . . . . 15 wff ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)
48	47, 37, 21	wral 2912	. . . . . . . . . . . . . 14 wff ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)
49	48, 41, 24	crab 2916	. . . . . . . . . . . . 13 class {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}
50	20, 49	wceq 1483	. . . . . . . . . . . 12 wff 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}
51	36, 50	wa 384	. . . . . . . . . . 11 wff (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})
52	51, 33, 22	wrex 2913	. . . . . . . . . 10 wff ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})
53	32, 52	wo 383	. . . . . . . . 9 wff (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
54	53, 9, 6	wrex 2913	. . . . . . . 8 wff ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))
55	54, 7, 19	copab 4712	. . . . . . 7 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}
56	6, 55	cun 3572	. . . . . 6 class (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})
57	5, 4, 56	cmpt 4729	. . . . 5 class (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}))
58		vj	. . . . . . . . . . . 12 setvar 𝑗
59	58	cv 1482	. . . . . . . . . . 11 class 𝑗
60		cgoe 31315	. . . . . . . . . . 11 class ∈𝑔
61	34, 59, 60	co 6650	. . . . . . . . . 10 class (𝑖∈𝑔𝑗)
62	8, 61	wceq 1483	. . . . . . . . 9 wff 𝑥 = (𝑖∈𝑔𝑗)
63	34, 42	cfv 5888	. . . . . . . . . . . 12 class (𝑎‘𝑖)
64	59, 42	cfv 5888	. . . . . . . . . . . 12 class (𝑎‘𝑗)
65	3	cv 1482	. . . . . . . . . . . 12 class 𝑒
66	63, 64, 65	wbr 4653	. . . . . . . . . . 11 wff (𝑎‘𝑖)𝑒(𝑎‘𝑗)
67	66, 41, 24	crab 2916	. . . . . . . . . 10 class {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}
68	20, 67	wceq 1483	. . . . . . . . 9 wff 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}
69	62, 68	wa 384	. . . . . . . 8 wff (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})
70	69, 58, 22	wrex 2913	. . . . . . 7 wff ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})
71	70, 33, 22	wrex 2913	. . . . . 6 wff ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})
72	71, 7, 19	copab 4712	. . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}
73	57, 72	crdg 7505	. . . 4 class rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})})
74	22	csuc 5725	. . . 4 class suc ω
75	73, 74	cres 5116	. . 3 class (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω)
76	2, 3, 4, 4, 75	cmpt2 6652	. 2 class (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω))
77	1, 76	wceq 1483	1 wff Sat = (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∧ 𝑦 = ((𝑚 ↑𝑚 ω) ∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ ∀𝑧 ∈ 𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑𝑚 ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω))

This definition is referenced by: (None)