Metamath Proof Explorer

Definition 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.

The coding scheme for the wffs is defined so that

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

Ref Expression
Assertion df-sat ⊢ Sat = m ∈ V , e ∈ V ⟼ rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ 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 ∩ 2 nd ⁡ v
28 23 27 cdif class m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v
29 19 28 wceq wff y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v
30 18 29 wa wff x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v
31 30 9 5 wrex wff ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v
32 vi setvar i
33 32 cv setvar i
34 13 33 cgol class ∀ 𝑔 i 1 st ⁡ u
35 10 34 wceq wff x = ∀ 𝑔 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 ∪ a ↾ ω ∖ i
46 45 25 wcel wff i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
47 46 37 20 wral wff ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
48 47 36 23 crab class a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
49 19 48 wceq wff y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
50 35 49 wa wff x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
51 50 32 22 wrex wff ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
52 31 51 wo wff ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
53 52 8 5 wrex wff ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
54 53 6 7 copab class x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
55 5 54 cun class f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
56 4 2 55 cmpt class f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u
57 vj setvar j
58 cgoe class ∈ 𝑔
59 57 cv setvar j
60 33 59 58 co class i ∈ 𝑔 j
61 10 60 wceq wff x = i ∈ 𝑔 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 ∈ m ω | a ⁡ i e a ⁡ j
67 19 66 wceq wff y = a ∈ m ω | a ⁡ i e a ⁡ j
68 61 67 wa wff x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j
69 68 57 22 wrex wff ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j
70 69 32 22 wrex wff ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j
71 70 6 7 copab class x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j
72 56 71 crdg class rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j
73 22 csuc class suc ⁡ ω
74 72 73 cres class rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j ↾ suc ⁡ ω
75 1 3 2 2 74 cmpo class m ∈ V , e ∈ V ⟼ rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j ↾ suc ⁡ ω
76 0 75 wceq wff Sat = m ∈ V , e ∈ V ⟼ rec ⁡ f ∈ V ⟼ f ∪ x y | ∃ u ∈ f ∃ v ∈ f x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∧ y = m ω ∖ 2 nd ⁡ u ∩ 2 nd ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ∧ y = a ∈ m ω | ∀ z ∈ m i z ∪ a ↾ ω ∖ i ∈ 2 nd ⁡ u x y | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ∧ y = a ∈ m ω | a ⁡ i e a ⁡ j ↾ suc ⁡ ω