Metamath Proof Explorer

Definition df-mfitp

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

Ref Expression
Assertion df-mfitp 
|- mFromItp = ( t e. _V |-> ( f e. X_ a e. ( mSA ` t ) ( ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } ) ) |-> ( iota_ n e. ( ( mUV ` t ) ^pm ( ( mVL ` t ) X. ( mEx ` t ) ) ) A. m e. ( mVL ` t ) ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfitp 
 |-  mFromItp
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vf 
 |-  f
4 va 
 |-  a
5 cmsa 
 |-  mSA
6 1 cv 
 |-  t
7 6 5 cfv 
 |-  ( mSA ` t )
8 cmuv 
 |-  mUV
9 6 8 cfv 
 |-  ( mUV ` t )
10 c1st 
 |-  1st
11 6 10 cfv 
 |-  ( 1st ` t )
12 4 cv 
 |-  a
13 12 11 cfv 
 |-  ( ( 1st ` t ) ` a )
14 13 csn 
 |-  { ( ( 1st ` t ) ` a ) }
15 9 14 cima 
 |-  ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } )
16 cmap 
 |-  ^m
17 vi 
 |-  i
18 cmvrs 
 |-  mVars
19 6 18 cfv 
 |-  ( mVars ` t )
20 12 19 cfv 
 |-  ( ( mVars ` t ) ` a )
21 cmty 
 |-  mType
22 6 21 cfv 
 |-  ( mType ` t )
23 17 cv 
 |-  i
24 23 22 cfv 
 |-  ( ( mType ` t ) ` i )
25 24 csn 
 |-  { ( ( mType ` t ) ` i ) }
26 9 25 cima 
 |-  ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } )
27 17 20 26 cixp 
 |-  X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } )
28 15 27 16 co 
 |-  ( ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } ) )
29 4 7 28 cixp 
 |-  X_ a e. ( mSA ` t ) ( ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } ) )
30 vn 
 |-  n
31 cpm 
 |-  ^pm
32 cmvl 
 |-  mVL
33 6 32 cfv 
 |-  ( mVL ` t )
34 cmex 
 |-  mEx
35 6 34 cfv 
 |-  ( mEx ` t )
36 33 35 cxp 
 |-  ( ( mVL ` t ) X. ( mEx ` t ) )
37 9 36 31 co 
 |-  ( ( mUV ` t ) ^pm ( ( mVL ` t ) X. ( mEx ` t ) ) )
38 vm 
 |-  m
39 vv 
 |-  v
40 cmvar 
 |-  mVR
41 6 40 cfv 
 |-  ( mVR ` t )
42 38 cv 
 |-  m
43 cmvh 
 |-  mVH
44 6 43 cfv 
 |-  ( mVH ` t )
45 39 cv 
 |-  v
46 45 44 cfv 
 |-  ( ( mVH ` t ) ` v )
47 42 46 cop 
 |-  <. m , ( ( mVH ` t ) ` v ) >.
48 30 cv 
 |-  n
49 45 42 cfv 
 |-  ( m ` v )
50 47 49 48 wbr 
 |-  <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v )
51 50 39 41 wral 
 |-  A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v )
52 ve 
 |-  e
53 vg 
 |-  g
54 52 cv 
 |-  e
55 cmst 
 |-  mST
56 6 55 cfv 
 |-  ( mST ` t )
57 53 cv 
 |-  g
58 12 57 cop 
 |-  <. a , g >.
59 54 58 56 wbr 
 |-  e ( mST ` t ) <. a , g >.
60 42 54 cop 
 |-  <. m , e >.
61 3 cv 
 |-  f
62 23 44 cfv 
 |-  ( ( mVH ` t ) ` i )
63 62 57 cfv 
 |-  ( g ` ( ( mVH ` t ) ` i ) )
64 42 63 48 co 
 |-  ( m n ( g ` ( ( mVH ` t ) ` i ) ) )
65 17 20 64 cmpt 
 |-  ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) )
66 65 61 cfv 
 |-  ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) )
67 60 66 48 wbr 
 |-  <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) )
68 59 67 wi 
 |-  ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) )
69 68 53 wal 
 |-  A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) )
70 69 4 wal 
 |-  A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) )
71 70 52 wal 
 |-  A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) )
72 60 csn 
 |-  { <. m , e >. }
73 48 72 cima 
 |-  ( n " { <. m , e >. } )
74 cmesy 
 |-  mESyn
75 6 74 cfv 
 |-  ( mESyn ` t )
76 54 75 cfv 
 |-  ( ( mESyn ` t ) ` e )
77 42 76 cop 
 |-  <. m , ( ( mESyn ` t ) ` e ) >.
78 77 csn 
 |-  { <. m , ( ( mESyn ` t ) ` e ) >. }
79 48 78 cima 
 |-  ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } )
80 54 10 cfv 
 |-  ( 1st ` e )
81 80 csn 
 |-  { ( 1st ` e ) }
82 9 81 cima 
 |-  ( ( mUV ` t ) " { ( 1st ` e ) } )
83 79 82 cin 
 |-  ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
84 73 83 wceq 
 |-  ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
85 84 52 35 wral 
 |-  A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
86 51 71 85 w3a 
 |-  ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) )
87 86 38 33 wral 
 |-  A. m e. ( mVL ` t ) ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) )
88 87 30 37 crio 
 |-  ( iota_ n e. ( ( mUV ` t ) ^pm ( ( mVL ` t ) X. ( mEx ` t ) ) ) A. m e. ( mVL ` t ) ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) )
89 3 29 88 cmpt 
 |-  ( f e. X_ a e. ( mSA ` t ) ( ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } ) ) |-> ( iota_ n e. ( ( mUV ` t ) ^pm ( ( mVL ` t ) X. ( mEx ` t ) ) ) A. m e. ( mVL ` t ) ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) ) )
90 1 2 89 cmpt 
 |-  ( t e. _V |-> ( f e. X_ a e. ( mSA ` t ) ( ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } ) ) |-> ( iota_ n e. ( ( mUV ` t ) ^pm ( ( mVL ` t ) X. ( mEx ` t ) ) ) A. m e. ( mVL ` t ) ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) ) ) )
91 0 90 wceq 
 |-  mFromItp = ( t e. _V |-> ( f e. X_ a e. ( mSA ` t ) ( ( ( mUV ` t ) " { ( ( 1st ` t ) ` a ) } ) ^m X_ i e. ( ( mVars ` t ) ` a ) ( ( mUV ` t ) " { ( ( mType ` t ) ` i ) } ) ) |-> ( iota_ n e. ( ( mUV ` t ) ^pm ( ( mVL ` t ) X. ( mEx ` t ) ) ) A. m e. ( mVL ` t ) ( A. v e. ( mVR ` t ) <. m , ( ( mVH ` t ) ` v ) >. n ( m ` v ) /\ A. e A. a A. g ( e ( mST ` t ) <. a , g >. -> <. m , e >. n ( f ` ( i e. ( ( mVars ` t ) ` a ) |-> ( m n ( g ` ( ( mVH ` t ) ` i ) ) ) ) ) ) /\ A. e e. ( mEx ` t ) ( n " { <. m , e >. } ) = ( ( n " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) ) ) )