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 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 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csat	|- Sat
1		vm	|- m
2		cvv	|- _V
3		ve	|- e
4		vf	|- f
5	4	cv	|- f
6		vx	|- x
7		vy	|- y
8		vu	|- u
9		vv	|- v
10	6	cv	|- x
11		c1st	|- 1st
12	8	cv	|- u
13	12 11	cfv	|- ( 1st ` u )
14		cgna	|- |g
15	9	cv	|- v
16	15 11	cfv	|- ( 1st ` v )
17	13 16 14	co	|- ( ( 1st ` u ) |g ( 1st ` v ) )
18	10 17	wceq	|- x = ( ( 1st ` u ) |g ( 1st ` v ) )
19	7	cv	|- y
20	1	cv	|- m
21		cmap	|- ^m
22		com	|- _om
23	20 22 21	co	|- ( m ^m _om )
24		c2nd	|- 2nd
25	12 24	cfv	|- ( 2nd ` u )
26	15 24	cfv	|- ( 2nd ` v )
27	25 26	cin	|- ( ( 2nd ` u ) i^i ( 2nd ` v ) )
28	23 27	cdif	|- ( ( m ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
29	19 28	wceq	|- y = ( ( m ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
30	18 29	wa	|- ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( m ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
31	30 9 5	wrex	|- E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( m ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
32		vi	|- i
33	32	cv	|- i
34	13 33	cgol	|- A.g i ( 1st ` u )
35	10 34	wceq	|- x = A.g i ( 1st ` u )
36		va	|- a
37		vz	|- z
38	37	cv	|- z
39	33 38	cop	|- <. i , z >.
40	39	csn	|- { <. i , z >. }
41	36	cv	|- a
42	33	csn	|- { i }
43	22 42	cdif	|- ( _om \ { i } )
44	41 43	cres	|- ( a |` ( _om \ { i } ) )
45	40 44	cun	|- ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) )
46	45 25	wcel	|- ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u )
47	46 37 20	wral	|- A. z e. m ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u )
48	47 36 23	crab	|- { a e. ( m ^m _om ) | A. z e. m ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
49	19 48	wceq	|- y = { a e. ( m ^m _om ) | A. z e. m ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
50	35 49	wa	|- ( 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 ) } )
51	50 32 22	wrex	|- 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 ) } )
52	31 51	wo	|- ( 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 ) } ) )
53	52 8 5	wrex	|- 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 ) } ) )
54	53 6 7	copab	|- { <. 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 ) } ) ) }
55	5 54	cun	|- ( 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 ) } ) ) } )
56	4 2 55	cmpt	|- ( 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 ) } ) ) } ) )
57		vj	|- j
58		cgoe	|- e.g
59	57	cv	|- j
60	33 59 58	co	|- ( i e.g j )
61	10 60	wceq	|- x = ( i e.g j )
62	33 41	cfv	|- ( a ` i )
63	3	cv	|- e
64	59 41	cfv	|- ( a ` j )
65	62 64 63	wbr	|- ( a ` i ) e ( a ` j )
66	65 36 23	crab	|- { a e. ( m ^m _om ) | ( a ` i ) e ( a ` j ) }
67	19 66	wceq	|- y = { a e. ( m ^m _om ) | ( a ` i ) e ( a ` j ) }
68	61 67	wa	|- ( x = ( i e.g j ) /\ y = { a e. ( m ^m _om ) | ( a ` i ) e ( a ` j ) } )
69	68 57 22	wrex	|- E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( m ^m _om ) | ( a ` i ) e ( a ` j ) } )
70	69 32 22	wrex	|- E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( m ^m _om ) | ( a ` i ) e ( a ` j ) } )
71	70 6 7	copab	|- { <. 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 ) } ) }
72	56 71	crdg	|- 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 ) } ) } )
73	22	csuc	|- suc _om
74	72 73	cres	|- ( 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 )
75	1 3 2 2 74	cmpo	|- ( 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 ) )
76	0 75	wceq	|- 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 ) )