df-sat

Description: Define the satisfaction predicate. This recursive construction builds up a function over wff codes (see satff ) and simultaneously defines the set of assignments to all variables from M that makes the coded wff true in the model M , where e. is interpreted as the binary relation E on M .

The interpretation of the statement S e. ( ( ( M Sat E )n )U ) is that for the model <. M , E >. , S :om --> M is a valuation of the variables (v0 = ( S(/) ) , v_1 = ( S1o ) , etc.) and U is a code for a wff using e. , -/\ , A. that is true under the assignment S . The function is defined by finite recursion; ( ( M Sat E )n ) only operates on wffs of depth at most n e.om , and ( ( M Sat E )om ) = U_ n e. _om ( ( M Sat E )n ) operates on all wffs.

		Ref	Expression
	Assertion	df-sat	$⊢ Sat = (m \in V, e \in V ⟼ {rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\}) ↾}_{suc ω})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csat	$class Sat$
1		vm	$setvar m$
2		cvv	$class V$
3		ve	$setvar e$
4		vf	$setvar f$
5	4	cv	$setvar f$
6		vx	$setvar x$
7		vy	$setvar y$
8		vu	$setvar u$
9		vv	$setvar v$
10	6	cv	$setvar x$
11		c1st	$class 1^{st}$
12	8	cv	$setvar u$
13	12 11	cfv	$class 1^{st} (u)$
14		cgna	$class ⊼_{𝑔}$
15	9	cv	$setvar v$
16	15 11	cfv	$class 1^{st} (v)$
17	13 16 14	co	$class (1^{st} (u) ⊼_{𝑔} 1^{st} (v))$
18	10 17	wceq	$wff x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v)$
19	7	cv	$setvar y$
20	1	cv	$setvar m$
21		cmap	$class ↑_{𝑚}$
22		com	$class ω$
23	20 22 21	co	$class (m^{ω})$
24		c2nd	$class 2^{nd}$
25	12 24	cfv	$class 2^{nd} (u)$
26	15 24	cfv	$class 2^{nd} (v)$
27	25 26	cin	$class (2^{nd} (u) \cap 2^{nd} (v))$
28	23 27	cdif	$class ((m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
29	19 28	wceq	$wff y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
30	18 29	wa	$wff (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
31	30 9 5	wrex	$wff \exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
32		vi	$setvar i$
33	32	cv	$setvar i$
34	13 33	cgol	$class [\forall_{𝑔} i 1^{st} (u)]$
35	10 34	wceq	$wff x = [\forall_{𝑔} i 1^{st} (u)]$
36		va	$setvar a$
37		vz	$setvar z$
38	37	cv	$setvar z$
39	33 38	cop	$class ⟨i, z⟩$
40	39	csn	$class \{⟨i, z⟩\}$
41	36	cv	$setvar a$
42	33	csn	$class \{i\}$
43	22 42	cdif	$class (ω ∖ \{i\})$
44	41 43	cres	$class ({a ↾}_{(ω ∖ \{i\})})$
45	40 44	cun	$class (\{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}))$
46	45 25	wcel	$wff \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)$
47	46 37 20	wral	$wff \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)$
48	47 36 23	crab	$class \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
49	19 48	wceq	$wff y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
50	35 49	wa	$wff (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
51	50 32 22	wrex	$wff \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
52	31 51	wo	$wff (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
53	52 8 5	wrex	$wff \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
54	53 6 7	copab	$class \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}$
55	5 54	cun	$class (f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
56	4 2 55	cmpt	$class (f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\})$
57		vj	$setvar j$
58		cgoe	$class \in_{𝑔}$
59	57	cv	$setvar j$
60	33 59 58	co	$class (i \in_{𝑔} j)$
61	10 60	wceq	$wff x = i \in_{𝑔} j$
62	33 41	cfv	$class a (i)$
63	3	cv	$setvar e$
64	59 41	cfv	$class a (j)$
65	62 64 63	wbr	$wff a (i) e a (j)$
66	65 36 23	crab	$class \{a \in (m^{ω}) \| a (i) e a (j)\}$
67	19 66	wceq	$wff y = \{a \in (m^{ω}) \| a (i) e a (j)\}$
68	61 67	wa	$wff (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})$
69	68 57 22	wrex	$wff \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})$
70	69 32 22	wrex	$wff \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})$
71	70 6 7	copab	$class \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\}$
72	56 71	crdg	$class rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\})$
73	22	csuc	$class suc ω$
74	72 73	cres	$class ({rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\}) ↾}_{suc ω})$
75	1 3 2 2 74	cmpo	$class (m \in V, e \in V ⟼ {rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\}) ↾}_{suc ω})$
76	0 75	wceq	$wff Sat = (m \in V, e \in V ⟼ {rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\}) ↾}_{suc ω})$

Metamath Proof Explorer

Definition df-sat

Detailed syntax breakdown