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

Definition df-sat 25030
 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 is that for the model , is a valuation of the variables (v0 , v1 , etc.) and is a code for a wff using that is true under the assignment . The function is defined by finite recursion; only operates on wffs of depth at most , and operates on all wffs. The coding scheme for the wffs is defined so that vi vj is coded as , is coded as , and vi is coded as . (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-sat
Distinct variable group:   ,,,,,,,,,,

Detailed syntax breakdown of Definition df-sat
StepHypRef Expression
1 csat 25023 . 2
2 vm . . 3
3 ve . . 3
4 cvv 2956 . . 3
5 vf . . . . . 6
65cv 1651 . . . . . . 7
7 vx . . . . . . . . . . . . . 14
87cv 1651 . . . . . . . . . . . . 13
9 vu . . . . . . . . . . . . . . . 16
109cv 1651 . . . . . . . . . . . . . . 15
11 c1st 6347 . . . . . . . . . . . . . . 15
1210, 11cfv 5454 . . . . . . . . . . . . . 14
13 vv . . . . . . . . . . . . . . . 16
1413cv 1651 . . . . . . . . . . . . . . 15
1514, 11cfv 5454 . . . . . . . . . . . . . 14
16 cgna 25021 . . . . . . . . . . . . . 14
1712, 15, 16co 6081 . . . . . . . . . . . . 13
188, 17wceq 1652 . . . . . . . . . . . 12
19 vy . . . . . . . . . . . . . 14
2019cv 1651 . . . . . . . . . . . . 13
212cv 1651 . . . . . . . . . . . . . . 15
22 com 4845 . . . . . . . . . . . . . . 15
23 cmap 7018 . . . . . . . . . . . . . . 15
2421, 22, 23co 6081 . . . . . . . . . . . . . 14
25 c2nd 6348 . . . . . . . . . . . . . . . 16
2610, 25cfv 5454 . . . . . . . . . . . . . . 15
2714, 25cfv 5454 . . . . . . . . . . . . . . 15
2826, 27cin 3319 . . . . . . . . . . . . . 14
2924, 28cdif 3317 . . . . . . . . . . . . 13
3020, 29wceq 1652 . . . . . . . . . . . 12
3118, 30wa 359 . . . . . . . . . . 11
3231, 13, 6wrex 2706 . . . . . . . . . 10
33 vi . . . . . . . . . . . . . . 15
3433cv 1651 . . . . . . . . . . . . . 14
3512, 34cgol 25022 . . . . . . . . . . . . 13
368, 35wceq 1652 . . . . . . . . . . . 12
37 vz . . . . . . . . . . . . . . . . . . . 20
3837cv 1651 . . . . . . . . . . . . . . . . . . 19
3934, 38cop 3817 . . . . . . . . . . . . . . . . . 18
4039csn 3814 . . . . . . . . . . . . . . . . 17
41 va . . . . . . . . . . . . . . . . . . 19
4241cv 1651 . . . . . . . . . . . . . . . . . 18
4334csn 3814 . . . . . . . . . . . . . . . . . . 19
4422, 43cdif 3317 . . . . . . . . . . . . . . . . . 18
4542, 44cres 4880 . . . . . . . . . . . . . . . . 17
4640, 45cun 3318 . . . . . . . . . . . . . . . 16
4746, 26wcel 1725 . . . . . . . . . . . . . . 15
4847, 37, 21wral 2705 . . . . . . . . . . . . . 14
4948, 41, 24crab 2709 . . . . . . . . . . . . 13
5020, 49wceq 1652 . . . . . . . . . . . 12
5136, 50wa 359 . . . . . . . . . . 11
5251, 33, 22wrex 2706 . . . . . . . . . 10
5332, 52wo 358 . . . . . . . . 9
5453, 9, 6wrex 2706 . . . . . . . 8
5554, 7, 19copab 4265 . . . . . . 7
566, 55cun 3318 . . . . . 6
575, 4, 56cmpt 4266 . . . . 5
58 vj . . . . . . . . . . . 12
5958cv 1651 . . . . . . . . . . 11
60 cgoe 25020 . . . . . . . . . . 11
6134, 59, 60co 6081 . . . . . . . . . 10
628, 61wceq 1652 . . . . . . . . 9
6334, 42cfv 5454 . . . . . . . . . . . 12
6459, 42cfv 5454 . . . . . . . . . . . 12
653cv 1651 . . . . . . . . . . . 12
6663, 64, 65wbr 4212 . . . . . . . . . . 11
6766, 41, 24crab 2709 . . . . . . . . . 10
6820, 67wceq 1652 . . . . . . . . 9
6962, 68wa 359 . . . . . . . 8
7069, 58, 22wrex 2706 . . . . . . 7
7170, 33, 22wrex 2706 . . . . . 6
7271, 7, 19copab 4265 . . . . 5
7357, 72crdg 6667 . . . 4
7422csuc 4583 . . . 4
7573, 74cres 4880 . . 3
762, 3, 4, 4, 75cmpt2 6083 . 2
771, 76wceq 1652 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator