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

Definition df-sat 23926
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  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 an valuation of the variables (v0  =  ( S `  (/) ), v1  =  ( S `  1o ), 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
  • vi  e. vj is coded as  <. (/) ,  <. i ,  j >. >.,
  •  ( ph  -/\  ps ) is coded as  <. 1o ,  <. ph ,  ps >. >., and
  •  A. vi  ph is coded as  <. 2o ,  <. i ,  ph >. >..

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

Assertion
Ref Expression
df-sat  |-  Sat  =  ( m  e.  _V ,  e  e.  _V  |->  ( rec ( ( f  e.  _V  |->  ( f  u.  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f 
( x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) ) )  \/  E. i  e. 
om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } ) ) ,  { <. x ,  y >.  |  E. i  e.  om  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } ) } )  |`  suc  om ) )
Distinct variable group:    e, a, f, i, j, m, u, v, x, y, z

Detailed syntax breakdown of Definition df-sat
StepHypRef Expression
1 csat 23919 . 2  class  Sat
2 vm . . 3  set  m
3 ve . . 3  set  e
4 cvv 2788 . . 3  class  _V
5 vf . . . . . 6  set  f
65cv 1622 . . . . . . 7  class  f
7 vx . . . . . . . . . . . . . 14  set  x
87cv 1622 . . . . . . . . . . . . 13  class  x
9 vu . . . . . . . . . . . . . . . 16  set  u
109cv 1622 . . . . . . . . . . . . . . 15  class  u
11 c1st 6120 . . . . . . . . . . . . . . 15  class  1st
1210, 11cfv 5255 . . . . . . . . . . . . . 14  class  ( 1st `  u )
13 vv . . . . . . . . . . . . . . . 16  set  v
1413cv 1622 . . . . . . . . . . . . . . 15  class  v
1514, 11cfv 5255 . . . . . . . . . . . . . 14  class  ( 1st `  v )
16 cgna 23917 . . . . . . . . . . . . . 14  class  | g
1712, 15, 16co 5858 . . . . . . . . . . . . 13  class  ( ( 1st `  u ) 
| g  ( 1st `  v ) )
188, 17wceq 1623 . . . . . . . . . . . 12  wff  x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )
19 vy . . . . . . . . . . . . . 14  set  y
2019cv 1622 . . . . . . . . . . . . 13  class  y
212cv 1622 . . . . . . . . . . . . . . 15  class  m
22 com 4656 . . . . . . . . . . . . . . 15  class  om
23 cmap 6772 . . . . . . . . . . . . . . 15  class  ^m
2421, 22, 23co 5858 . . . . . . . . . . . . . 14  class  ( m  ^m  om )
25 c2nd 6121 . . . . . . . . . . . . . . . 16  class  2nd
2610, 25cfv 5255 . . . . . . . . . . . . . . 15  class  ( 2nd `  u )
2714, 25cfv 5255 . . . . . . . . . . . . . . 15  class  ( 2nd `  v )
2826, 27cin 3151 . . . . . . . . . . . . . 14  class  ( ( 2nd `  u )  i^i  ( 2nd `  v
) )
2924, 28cdif 3149 . . . . . . . . . . . . 13  class  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v ) ) )
3020, 29wceq 1623 . . . . . . . . . . . 12  wff  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) )
3118, 30wa 358 . . . . . . . . . . 11  wff  ( x  =  ( ( 1st `  u )  | g 
( 1st `  v
) )  /\  y  =  ( ( m  ^m  om )  \ 
( ( 2nd `  u
)  i^i  ( 2nd `  v ) ) ) )
3231, 13, 6wrex 2544 . . . . . . . . . 10  wff  E. v  e.  f  ( x  =  ( ( 1st `  u )  | g 
( 1st `  v
) )  /\  y  =  ( ( m  ^m  om )  \ 
( ( 2nd `  u
)  i^i  ( 2nd `  v ) ) ) )
33 vi . . . . . . . . . . . . . . 15  set  i
3433cv 1622 . . . . . . . . . . . . . 14  class  i
3512, 34cgol 23918 . . . . . . . . . . . . 13  class  A.g i
( 1st `  u
)
368, 35wceq 1623 . . . . . . . . . . . 12  wff  x  = 
A.g i ( 1st `  u )
37 vz . . . . . . . . . . . . . . . . . . . 20  set  z
3837cv 1622 . . . . . . . . . . . . . . . . . . 19  class  z
3934, 38cop 3643 . . . . . . . . . . . . . . . . . 18  class  <. i ,  z >.
4039csn 3640 . . . . . . . . . . . . . . . . 17  class  { <. i ,  z >. }
41 va . . . . . . . . . . . . . . . . . . 19  set  a
4241cv 1622 . . . . . . . . . . . . . . . . . 18  class  a
4334csn 3640 . . . . . . . . . . . . . . . . . . 19  class  { i }
4422, 43cdif 3149 . . . . . . . . . . . . . . . . . 18  class  ( om 
\  { i } )
4542, 44cres 4691 . . . . . . . . . . . . . . . . 17  class  ( a  |`  ( om  \  {
i } ) )
4640, 45cun 3150 . . . . . . . . . . . . . . . 16  class  ( {
<. i ,  z >. }  u.  ( a  |`  ( om  \  {
i } ) ) )
4746, 26wcel 1684 . . . . . . . . . . . . . . 15  wff  ( {
<. i ,  z >. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u )
4847, 37, 21wral 2543 . . . . . . . . . . . . . 14  wff  A. z  e.  m  ( { <. i ,  z >. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u )
4948, 41, 24crab 2547 . . . . . . . . . . . . 13  class  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z >. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) }
5020, 49wceq 1623 . . . . . . . . . . . 12  wff  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) }
5136, 50wa 358 . . . . . . . . . . 11  wff  ( x  =  A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } )
5251, 33, 22wrex 2544 . . . . . . . . . 10  wff  E. i  e.  om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } )
5332, 52wo 357 . . . . . . . . 9  wff  ( E. v  e.  f  ( x  =  ( ( 1st `  u ) 
| g  ( 1st `  v ) )  /\  y  =  ( (
m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v ) ) ) )  \/  E. i  e.  om  (
x  =  A.g i
( 1st `  u
)  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) )
5453, 9, 6wrex 2544 . . . . . . . 8  wff  E. u  e.  f  ( E. v  e.  f  (
x  =  ( ( 1st `  u ) 
| g  ( 1st `  v ) )  /\  y  =  ( (
m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v ) ) ) )  \/  E. i  e.  om  (
x  =  A.g i
( 1st `  u
)  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) )
5554, 7, 19copab 4076 . . . . . . 7  class  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f 
( x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) ) )  \/  E. i  e. 
om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) }
566, 55cun 3150 . . . . . 6  class  ( f  u.  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f 
( x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) ) )  \/  E. i  e. 
om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } )
575, 4, 56cmpt 4077 . . . . 5  class  ( f  e.  _V  |->  ( f  u.  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f 
( x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) ) )  \/  E. i  e. 
om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } ) )
58 vj . . . . . . . . . . . 12  set  j
5958cv 1622 . . . . . . . . . . 11  class  j
60 cgoe 23916 . . . . . . . . . . 11  class  e.g
6134, 59, 60co 5858 . . . . . . . . . 10  class  ( i  e.g  j )
628, 61wceq 1623 . . . . . . . . 9  wff  x  =  ( i  e.g  j
)
6334, 42cfv 5255 . . . . . . . . . . . 12  class  ( a `
 i )
6459, 42cfv 5255 . . . . . . . . . . . 12  class  ( a `
 j )
653cv 1622 . . . . . . . . . . . 12  class  e
6663, 64, 65wbr 4023 . . . . . . . . . . 11  wff  ( a `
 i ) e ( a `  j
)
6766, 41, 24crab 2547 . . . . . . . . . 10  class  { a  e.  ( m  ^m  om )  |  ( a `
 i ) e ( a `  j
) }
6820, 67wceq 1623 . . . . . . . . 9  wff  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) }
6962, 68wa 358 . . . . . . . 8  wff  ( x  =  ( i  e.g  j )  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } )
7069, 58, 22wrex 2544 . . . . . . 7  wff  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } )
7170, 33, 22wrex 2544 . . . . . 6  wff  E. i  e.  om  E. j  e. 
om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } )
7271, 7, 19copab 4076 . . . . 5  class  { <. x ,  y >.  |  E. i  e.  om  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } ) }
7357, 72crdg 6422 . . . 4  class  rec (
( f  e.  _V  |->  ( f  u.  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f  ( x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) ) )  \/  E. i  e. 
om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } ) ) ,  { <. x ,  y >.  |  E. i  e.  om  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } ) } )
7422csuc 4394 . . . 4  class  suc  om
7573, 74cres 4691 . . 3  class  ( rec ( ( f  e. 
_V  |->  ( f  u. 
{ <. x ,  y
>.  |  E. u  e.  f  ( E. v  e.  f  (
x  =  ( ( 1st `  u ) 
| g  ( 1st `  v ) )  /\  y  =  ( (
m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v ) ) ) )  \/  E. i  e.  om  (
x  =  A.g i
( 1st `  u
)  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } ) ) ,  { <. x ,  y >.  |  E. i  e.  om  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } ) } )  |`  suc  om )
762, 3, 4, 4, 75cmpt2 5860 . 2  class  ( m  e.  _V ,  e  e.  _V  |->  ( rec ( ( f  e. 
_V  |->  ( f  u. 
{ <. x ,  y
>.  |  E. u  e.  f  ( E. v  e.  f  (
x  =  ( ( 1st `  u ) 
| g  ( 1st `  v ) )  /\  y  =  ( (
m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v ) ) ) )  \/  E. i  e.  om  (
x  =  A.g i
( 1st `  u
)  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } ) ) ,  { <. x ,  y >.  |  E. i  e.  om  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } ) } )  |`  suc  om ) )
771, 76wceq 1623 1  wff  Sat  =  ( m  e.  _V ,  e  e.  _V  |->  ( rec ( ( f  e.  _V  |->  ( f  u.  { <. x ,  y >.  |  E. u  e.  f  ( E. v  e.  f 
( x  =  ( ( 1st `  u
)  | g  ( 1st `  v ) )  /\  y  =  ( ( m  ^m  om )  \  ( ( 2nd `  u )  i^i  ( 2nd `  v
) ) ) )  \/  E. i  e. 
om  ( x  = 
A.g i ( 1st `  u )  /\  y  =  { a  e.  ( m  ^m  om )  |  A. z  e.  m  ( { <. i ,  z
>. }  u.  ( a  |`  ( om  \  {
i } ) ) )  e.  ( 2nd `  u ) } ) ) } ) ) ,  { <. x ,  y >.  |  E. i  e.  om  E. j  e.  om  ( x  =  ( i  e.g  j
)  /\  y  =  { a  e.  ( m  ^m  om )  |  ( a `  i ) e ( a `  j ) } ) } )  |`  suc  om ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator