Definition df-sat 31325

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 a valuation of the variables (v₀ = ( S ` (/) ), v<sub>1</sub> = ( 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

• v_i e. v_j is coded as <. (/) , <. i , j >. >.,
• ( ph -/\ ps ) is coded as <. 1o , <. ph , ps >. >., and
• A. v_i 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

Step	Hyp	Ref	Expression
1		csat 31318	. 2 class Sat
2		vm	. . 3 setvar m
3		ve	. . 3 setvar e
4		cvv 3200	. . 3 class _V
5		vf	. . . . . 6 setvar f
6	5	cv 1482	. . . . . . 7 class f
7		vx	. . . . . . . . . . . . . 14 setvar x
8	7	cv 1482	. . . . . . . . . . . . 13 class x
9		vu	. . . . . . . . . . . . . . . 16 setvar u
10	9	cv 1482	. . . . . . . . . . . . . . 15 class u
11		c1st 7166	. . . . . . . . . . . . . . 15 class 1st
12	10, 11	cfv 5888	. . . . . . . . . . . . . 14 class ( 1st ` u )
13		vv	. . . . . . . . . . . . . . . 16 setvar v
14	13	cv 1482	. . . . . . . . . . . . . . 15 class v
15	14, 11	cfv 5888	. . . . . . . . . . . . . 14 class ( 1st ` v )
16		cgna 31316	. . . . . . . . . . . . . 14 class |g
17	12, 15, 16	co 6650	. . . . . . . . . . . . 13 class ( ( 1st ` u ) |g ( 1st ` v ) )
18	8, 17	wceq 1483	. . . . . . . . . . . 12 wff x = ( ( 1st ` u ) |g ( 1st ` v ) )
19		vy	. . . . . . . . . . . . . 14 setvar y
20	19	cv 1482	. . . . . . . . . . . . 13 class y
21	2	cv 1482	. . . . . . . . . . . . . . 15 class m
22		com 7065	. . . . . . . . . . . . . . 15 class om
23		cmap 7857	. . . . . . . . . . . . . . 15 class ^m
24	21, 22, 23	co 6650	. . . . . . . . . . . . . 14 class ( m ^m om )
25		c2nd 7167	. . . . . . . . . . . . . . . 16 class 2nd
26	10, 25	cfv 5888	. . . . . . . . . . . . . . 15 class ( 2nd ` u )
27	14, 25	cfv 5888	. . . . . . . . . . . . . . 15 class ( 2nd ` v )
28	26, 27	cin 3573	. . . . . . . . . . . . . 14 class ( ( 2nd ` u ) i^i ( 2nd ` v ) )
29	24, 28	cdif 3571	. . . . . . . . . . . . 13 class ( ( m ^m om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
30	20, 29	wceq 1483	. . . . . . . . . . . 12 wff y = ( ( m ^m om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
31	18, 30	wa 384	. . . . . . . . . . 11 wff ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( m ^m om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
32	31, 13, 6	wrex 2913	. . . . . . . . . 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 setvar i
34	33	cv 1482	. . . . . . . . . . . . . 14 class i
35	12, 34	cgol 31317	. . . . . . . . . . . . 13 class A.g i ( 1st ` u )
36	8, 35	wceq 1483	. . . . . . . . . . . 12 wff x = A.g i ( 1st ` u )
37		vz	. . . . . . . . . . . . . . . . . . . 20 setvar z
38	37	cv 1482	. . . . . . . . . . . . . . . . . . 19 class z
39	34, 38	cop 4183	. . . . . . . . . . . . . . . . . 18 class <. i , z >.
40	39	csn 4177	. . . . . . . . . . . . . . . . 17 class { <. i , z >. }
41		va	. . . . . . . . . . . . . . . . . . 19 setvar a
42	41	cv 1482	. . . . . . . . . . . . . . . . . 18 class a
43	34	csn 4177	. . . . . . . . . . . . . . . . . . 19 class { i }
44	22, 43	cdif 3571	. . . . . . . . . . . . . . . . . 18 class ( om \ { i } )
45	42, 44	cres 5116	. . . . . . . . . . . . . . . . 17 class ( a |` ( om \ { i } ) )
46	40, 45	cun 3572	. . . . . . . . . . . . . . . 16 class ( { <. i , z >. } u. ( a |` ( om \ { i } ) ) )
47	46, 26	wcel 1990	. . . . . . . . . . . . . . 15 wff ( { <. i , z >. } u. ( a |` ( om \ { i } ) ) ) e. ( 2nd ` u )
48	47, 37, 21	wral 2912	. . . . . . . . . . . . . 14 wff A. z e. m ( { <. i , z >. } u. ( a |` ( om \ { i } ) ) ) e. ( 2nd ` u )
49	48, 41, 24	crab 2916	. . . . . . . . . . . . 13 class { a e. ( m ^m om ) | A. z e. m ( { <. i , z >. } u. ( a |` ( om \ { i } ) ) ) e. ( 2nd ` u ) }
50	20, 49	wceq 1483	. . . . . . . . . . . 12 wff y = { a e. ( m ^m om ) | A. z e. m ( { <. i , z >. } u. ( a |` ( om \ { i } ) ) ) e. ( 2nd ` u ) }
51	36, 50	wa 384	. . . . . . . . . . 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 ) } )
52	51, 33, 22	wrex 2913	. . . . . . . . . 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 ) } )
53	32, 52	wo 383	. . . . . . . . 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 ) } ) )
54	53, 9, 6	wrex 2913	. . . . . . . 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 ) } ) )
55	54, 7, 19	copab 4712	. . . . . . 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 ) } ) ) }
56	6, 55	cun 3572	. . . . . 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 ) } ) ) } )
57	5, 4, 56	cmpt 4729	. . . . 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 setvar j
59	58	cv 1482	. . . . . . . . . . 11 class j
60		cgoe 31315	. . . . . . . . . . 11 class e.g
61	34, 59, 60	co 6650	. . . . . . . . . 10 class ( i e.g j )
62	8, 61	wceq 1483	. . . . . . . . 9 wff x = ( i e.g j )
63	34, 42	cfv 5888	. . . . . . . . . . . 12 class ( a ` i )
64	59, 42	cfv 5888	. . . . . . . . . . . 12 class ( a ` j )
65	3	cv 1482	. . . . . . . . . . . 12 class e
66	63, 64, 65	wbr 4653	. . . . . . . . . . 11 wff ( a ` i ) e ( a ` j )
67	66, 41, 24	crab 2916	. . . . . . . . . 10 class { a e. ( m ^m om ) | ( a ` i ) e ( a ` j ) }
68	20, 67	wceq 1483	. . . . . . . . 9 wff y = { a e. ( m ^m om ) | ( a ` i ) e ( a ` j ) }
69	62, 68	wa 384	. . . . . . . 8 wff ( x = ( i e.g j ) /\ y = { a e. ( m ^m om ) | ( a ` i ) e ( a ` j ) } )
70	69, 58, 22	wrex 2913	. . . . . . 7 wff E. j e. om ( x = ( i e.g j ) /\ y = { a e. ( m ^m om ) | ( a ` i ) e ( a ` j ) } )
71	70, 33, 22	wrex 2913	. . . . . 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 ) } )
72	71, 7, 19	copab 4712	. . . . 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 ) } ) }
73	57, 72	crdg 7505	. . . 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 ) } ) } )
74	22	csuc 5725	. . . 4 class suc om
75	73, 74	cres 5116	. . 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 )
76	2, 3, 4, 4, 75	cmpt2 6652	. 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 ) )
77	1, 76	wceq 1483	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 ) )

This definition is referenced by: (None)