Definition df-mfitp 31521

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

Assertion

Ref

Expression

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

Distinct variable group:   e, a, f, g, i, m, n, t, v

Detailed syntax breakdown of Definition df-mfitp

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

This definition is referenced by: (None)