Metamath Proof Explorer

Definition df-mitp

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

Ref Expression
Assertion 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmitp 
 |-  mItp
1 vt 
 |-  t
2 cvv 
 |-  _V
3 va 
 |-  a
4 cmsa 
 |-  mSA
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mSA ` t )
7 vg 
 |-  g
8 vi 
 |-  i
9 cmvrs 
 |-  mVars
10 5 9 cfv 
 |-  ( mVars ` t )
11 3 cv 
 |-  a
12 11 10 cfv 
 |-  ( ( mVars ` t ) ` a )
13 cmuv 
 |-  mUV
14 5 13 cfv 
 |-  ( mUV ` t )
15 cmty 
 |-  mType
16 5 15 cfv 
 |-  ( mType ` t )
17 8 cv 
 |-  i
18 17 16 cfv 
 |-  ( ( mType ` t ) ` i )
19 18 csn 
 |-  { ( ( mType ` t ) ` i ) }
20 14 19 cima 
 |-  ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } )
21 8 12 20 cixp 
 |-  X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } )
22 vx 
 |-  x
23 vm 
 |-  m
24 cmvl 
 |-  mVL
25 5 24 cfv 
 |-  ( mVL ` t )
26 7 cv 
 |-  g
27 23 cv 
 |-  m
28 27 12 cres 
 |-  ( m |` ( ( mVars ` t ) ` a ) )
29 26 28 wceq 
 |-  g = ( m |` ( ( mVars ` t ) ` a ) )
30 22 cv 
 |-  x
31 cmevl 
 |-  mEval
32 5 31 cfv 
 |-  ( mEval ` t )
33 27 11 32 co 
 |-  ( m ( mEval ` t ) a )
34 30 33 wceq 
 |-  x = ( m ( mEval ` t ) a )
35 29 34 wa 
 |-  ( g = ( m |` ( ( mVars ` t ) ` a ) ) /\ x = ( m ( mEval ` t ) a ) )
36 35 23 25 wrex 
 |-  E. m e. ( mVL ` t ) ( g = ( m |` ( ( mVars ` t ) ` a ) ) /\ x = ( m ( mEval ` t ) a ) )
37 36 22 cio 
 |-  ( iota x E. m e. ( mVL ` t ) ( g = ( m |` ( ( mVars ` t ) ` a ) ) /\ x = ( m ( mEval ` t ) a ) ) )
38 7 21 37 cmpt 
 |-  ( 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 ) ) ) )
39 3 6 38 cmpt 
 |-  ( 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 ) ) ) ) )
40 1 2 39 cmpt 
 |-  ( 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 ) ) ) ) ) )
41 0 40 wceq 
 |-  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 ) ) ) ) ) )