Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sat Structured version   Visualization version   GIF version

Definition df-sat 30579
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 (v0 = (𝑆‘∅), v1 = (𝑆‘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
  • vi vj is coded as ⟨∅, ⟨𝑖, 𝑗⟩⟩,
  • (𝜑𝜓) is coded as ⟨1𝑜, ⟨𝜑, 𝜓⟩⟩, and
  • vi 𝜑 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
StepHypRef Expression
1 csat 30572 . 2 class Sat
2 vm . . 3 setvar 𝑚
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
5 vf . . . . . 6 setvar 𝑓
65cv 1474 . . . . . . 7 class 𝑓
7 vx . . . . . . . . . . . . . 14 setvar 𝑥
87cv 1474 . . . . . . . . . . . . 13 class 𝑥
9 vu . . . . . . . . . . . . . . . 16 setvar 𝑢
109cv 1474 . . . . . . . . . . . . . . 15 class 𝑢
11 c1st 7057 . . . . . . . . . . . . . . 15 class 1st
1210, 11cfv 5804 . . . . . . . . . . . . . 14 class (1st𝑢)
13 vv . . . . . . . . . . . . . . . 16 setvar 𝑣
1413cv 1474 . . . . . . . . . . . . . . 15 class 𝑣
1514, 11cfv 5804 . . . . . . . . . . . . . 14 class (1st𝑣)
16 cgna 30570 . . . . . . . . . . . . . 14 class 𝑔
1712, 15, 16co 6549 . . . . . . . . . . . . 13 class ((1st𝑢)⊼𝑔(1st𝑣))
188, 17wceq 1475 . . . . . . . . . . . 12 wff 𝑥 = ((1st𝑢)⊼𝑔(1st𝑣))
19 vy . . . . . . . . . . . . . 14 setvar 𝑦
2019cv 1474 . . . . . . . . . . . . 13 class 𝑦
212cv 1474 . . . . . . . . . . . . . . 15 class 𝑚
22 com 6957 . . . . . . . . . . . . . . 15 class ω
23 cmap 7744 . . . . . . . . . . . . . . 15 class 𝑚
2421, 22, 23co 6549 . . . . . . . . . . . . . 14 class (𝑚𝑚 ω)
25 c2nd 7058 . . . . . . . . . . . . . . . 16 class 2nd
2610, 25cfv 5804 . . . . . . . . . . . . . . 15 class (2nd𝑢)
2714, 25cfv 5804 . . . . . . . . . . . . . . 15 class (2nd𝑣)
2826, 27cin 3539 . . . . . . . . . . . . . 14 class ((2nd𝑢) ∩ (2nd𝑣))
2924, 28cdif 3537 . . . . . . . . . . . . 13 class ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
3020, 29wceq 1475 . . . . . . . . . . . 12 wff 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))
3118, 30wa 383 . . . . . . . . . . 11 wff (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
3231, 13, 6wrex 2897 . . . . . . . . . 10 wff 𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣))))
33 vi . . . . . . . . . . . . . . 15 setvar 𝑖
3433cv 1474 . . . . . . . . . . . . . 14 class 𝑖
3512, 34cgol 30571 . . . . . . . . . . . . 13 class 𝑔𝑖(1st𝑢)
368, 35wceq 1475 . . . . . . . . . . . 12 wff 𝑥 = ∀𝑔𝑖(1st𝑢)
37 vz . . . . . . . . . . . . . . . . . . . 20 setvar 𝑧
3837cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑧
3934, 38cop 4131 . . . . . . . . . . . . . . . . . 18 class 𝑖, 𝑧
4039csn 4125 . . . . . . . . . . . . . . . . 17 class {⟨𝑖, 𝑧⟩}
41 va . . . . . . . . . . . . . . . . . . 19 setvar 𝑎
4241cv 1474 . . . . . . . . . . . . . . . . . 18 class 𝑎
4334csn 4125 . . . . . . . . . . . . . . . . . . 19 class {𝑖}
4422, 43cdif 3537 . . . . . . . . . . . . . . . . . 18 class (ω ∖ {𝑖})
4542, 44cres 5040 . . . . . . . . . . . . . . . . 17 class (𝑎 ↾ (ω ∖ {𝑖}))
4640, 45cun 3538 . . . . . . . . . . . . . . . 16 class ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖})))
4746, 26wcel 1977 . . . . . . . . . . . . . . 15 wff ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)
4847, 37, 21wral 2896 . . . . . . . . . . . . . 14 wff 𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)
4948, 41, 24crab 2900 . . . . . . . . . . . . 13 class {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
5020, 49wceq 1475 . . . . . . . . . . . 12 wff 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}
5136, 50wa 383 . . . . . . . . . . 11 wff (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
5251, 33, 22wrex 2897 . . . . . . . . . 10 wff 𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)})
5332, 52wo 382 . . . . . . . . 9 wff (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
5453, 9, 6wrex 2897 . . . . . . . 8 wff 𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))
5554, 7, 19copab 4642 . . . . . . 7 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}
566, 55cun 3538 . . . . . 6 class (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})
575, 4, 56cmpt 4643 . . . . 5 class (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
58 vj . . . . . . . . . . . 12 setvar 𝑗
5958cv 1474 . . . . . . . . . . 11 class 𝑗
60 cgoe 30569 . . . . . . . . . . 11 class 𝑔
6134, 59, 60co 6549 . . . . . . . . . 10 class (𝑖𝑔𝑗)
628, 61wceq 1475 . . . . . . . . 9 wff 𝑥 = (𝑖𝑔𝑗)
6334, 42cfv 5804 . . . . . . . . . . . 12 class (𝑎𝑖)
6459, 42cfv 5804 . . . . . . . . . . . 12 class (𝑎𝑗)
653cv 1474 . . . . . . . . . . . 12 class 𝑒
6663, 64, 65wbr 4583 . . . . . . . . . . 11 wff (𝑎𝑖)𝑒(𝑎𝑗)
6766, 41, 24crab 2900 . . . . . . . . . 10 class {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)}
6820, 67wceq 1475 . . . . . . . . 9 wff 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)}
6962, 68wa 383 . . . . . . . 8 wff (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})
7069, 58, 22wrex 2897 . . . . . . 7 wff 𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})
7170, 33, 22wrex 2897 . . . . . 6 wff 𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})
7271, 7, 19copab 4642 . . . . 5 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})}
7357, 72crdg 7392 . . . 4 class rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})})
7422csuc 5642 . . . 4 class suc ω
7573, 74cres 5040 . . 3 class (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})}) ↾ suc ω)
762, 3, 4, 4, 75cmpt2 6551 . 2 class (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})}) ↾ suc ω))
771, 76wceq 1475 1 wff Sat = (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑓 (∃𝑣𝑓 (𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑚𝑚 ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ ∀𝑧𝑚 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚𝑚 ω) ∣ (𝑎𝑖)𝑒(𝑎𝑗)})}) ↾ suc ω))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator