Definition df-mitp 31520

Description: Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-mitp	|- mItp = ( t e. _V |-> ( a e. (mSA ` t ) |-> ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) ) ) )

Distinct variable group:   g, a, i, m, t, x

Detailed syntax breakdown of Definition df-mitp

Step	Hyp	Ref	Expression
1		cmitp 31509	. 2 class mItp
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		va	. . . 4 setvar a
5	2	cv 1482	. . . . 5 class t
6		cmsa 31483	. . . . 5 class mSA
7	5, 6	cfv 5888	. . . 4 class (mSA ` t )
8		vg	. . . . 5 setvar g
9		vi	. . . . . 6 setvar i
10	4	cv 1482	. . . . . . 7 class a
11		cmvrs 31366	. . . . . . . 8 class mVars
12	5, 11	cfv 5888	. . . . . . 7 class (mVars ` t )
13	10, 12	cfv 5888	. . . . . 6 class ( (mVars ` t ) ` a )
14		cmuv 31500	. . . . . . . 8 class mUV
15	5, 14	cfv 5888	. . . . . . 7 class (mUV ` t )
16	9	cv 1482	. . . . . . . . 9 class i
17		cmty 31359	. . . . . . . . . 10 class mType
18	5, 17	cfv 5888	. . . . . . . . 9 class (mType ` t )
19	16, 18	cfv 5888	. . . . . . . 8 class ( (mType ` t ) ` i )
20	19	csn 4177	. . . . . . 7 class { ( (mType ` t ) ` i ) }
21	15, 20	cima 5117	. . . . . 6 class ( (mUV ` t ) " { ( (mType ` t ) ` i ) } )
22	9, 13, 21	cixp 7908	. . . . 5 class X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } )
23	8	cv 1482	. . . . . . . . 9 class g
24		vm	. . . . . . . . . . 11 setvar m
25	24	cv 1482	. . . . . . . . . 10 class m
26	25, 13	cres 5116	. . . . . . . . 9 class ( m |` ( (mVars ` t ) ` a ) )
27	23, 26	wceq 1483	. . . . . . . 8 wff g = ( m |` ( (mVars ` t ) ` a ) )
28		vx	. . . . . . . . . 10 setvar x
29	28	cv 1482	. . . . . . . . 9 class x
30		cmevl 31505	. . . . . . . . . . 11 class mEval
31	5, 30	cfv 5888	. . . . . . . . . 10 class (mEval ` t )
32	25, 10, 31	co 6650	. . . . . . . . 9 class ( m (mEval ` t ) a )
33	29, 32	wceq 1483	. . . . . . . 8 wff x = ( m (mEval ` t ) a )
34	27, 33	wa 384	. . . . . . 7 wff ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) )
35		cmvl 31501	. . . . . . . 8 class mVL
36	5, 35	cfv 5888	. . . . . . 7 class (mVL ` t )
37	34, 24, 36	wrex 2913	. . . . . 6 wff E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) )
38	37, 28	cio 5849	. . . . 5 class ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) )
39	8, 22, 38	cmpt 4729	. . . 4 class ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) )
40	4, 7, 39	cmpt 4729	. . 3 class ( a e. (mSA ` t ) |-> ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) ) )
41	2, 3, 40	cmpt 4729	. 2 class ( t e. _V |-> ( a e. (mSA ` t ) |-> ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) ) ) )
42	1, 41	wceq 1483	1 wff mItp = ( t e. _V |-> ( a e. (mSA ` t ) |-> ( g e. X_ i e. ( (mVars ` t ) ` a ) ( (mUV ` t ) " { ( (mType ` t ) ` i ) } ) |-> ( iota x E. m e. (mVL ` t ) ( g = ( m |` ( (mVars ` t ) ` a ) ) /\ x = ( m (mEval ` t ) a ) ) ) ) ) )

This definition is referenced by: (None)