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 = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ X 𝑎 ∈ ( mSA ‘ 𝑡 ) ( ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } ) ↑m X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ) ↦ ( ℩ 𝑛 ∈ ( ( mUV ‘ 𝑡 ) ↑pm ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) ) ) ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmfitp	⊢ mFromItp
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		va	⊢ 𝑎
5		cmsa	⊢ mSA
6	1	cv	⊢ 𝑡
7	6 5	cfv	⊢ ( mSA ‘ 𝑡 )
8		cmuv	⊢ mUV
9	6 8	cfv	⊢ ( mUV ‘ 𝑡 )
10		c1st	⊢ 1st
11	6 10	cfv	⊢ ( 1st ‘ 𝑡 )
12	4	cv	⊢ 𝑎
13	12 11	cfv	⊢ ( ( 1st ‘ 𝑡 ) ‘ 𝑎 )
14	13	csn	⊢ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) }
15	9 14	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } )
16		cmap	⊢ ↑m
17		vi	⊢ 𝑖
18		cmvrs	⊢ mVars
19	6 18	cfv	⊢ ( mVars ‘ 𝑡 )
20	12 19	cfv	⊢ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 )
21		cmty	⊢ mType
22	6 21	cfv	⊢ ( mType ‘ 𝑡 )
23	17	cv	⊢ 𝑖
24	23 22	cfv	⊢ ( ( mType ‘ 𝑡 ) ‘ 𝑖 )
25	24	csn	⊢ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) }
26	9 25	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } )
27	17 20 26	cixp	⊢ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } )
28	15 27 16	co	⊢ ( ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } ) ↑m X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) )
29	4 7 28	cixp	⊢ X 𝑎 ∈ ( mSA ‘ 𝑡 ) ( ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } ) ↑m X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) )
30		vn	⊢ 𝑛
31		cpm	⊢ ↑pm
32		cmvl	⊢ mVL
33	6 32	cfv	⊢ ( mVL ‘ 𝑡 )
34		cmex	⊢ mEx
35	6 34	cfv	⊢ ( mEx ‘ 𝑡 )
36	33 35	cxp	⊢ ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) )
37	9 36 31	co	⊢ ( ( mUV ‘ 𝑡 ) ↑pm ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) ) )
38		vm	⊢ 𝑚
39		vv	⊢ 𝑣
40		cmvar	⊢ mVR
41	6 40	cfv	⊢ ( mVR ‘ 𝑡 )
42	38	cv	⊢ 𝑚
43		cmvh	⊢ mVH
44	6 43	cfv	⊢ ( mVH ‘ 𝑡 )
45	39	cv	⊢ 𝑣
46	45 44	cfv	⊢ ( ( mVH ‘ 𝑡 ) ‘ 𝑣 )
47	42 46	cop	⊢ ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩
48	30	cv	⊢ 𝑛
49	45 42	cfv	⊢ ( 𝑚 ‘ 𝑣 )
50	47 49 48	wbr	⊢ ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 )
51	50 39 41	wral	⊢ ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 )
52		ve	⊢ 𝑒
53		vg	⊢ 𝑔
54	52	cv	⊢ 𝑒
55		cmst	⊢ mST
56	6 55	cfv	⊢ ( mST ‘ 𝑡 )
57	53	cv	⊢ 𝑔
58	12 57	cop	⊢ ⟨ 𝑎 , 𝑔 ⟩
59	54 58 56	wbr	⊢ 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩
60	42 54	cop	⊢ ⟨ 𝑚 , 𝑒 ⟩
61	3	cv	⊢ 𝑓
62	23 44	cfv	⊢ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 )
63	62 57	cfv	⊢ ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) )
64	42 63 48	co	⊢ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) )
65	17 20 64	cmpt	⊢ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) )
66	65 61	cfv	⊢ ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) )
67	60 66 48	wbr	⊢ ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) )
68	59 67	wi	⊢ ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) )
69	68 53	wal	⊢ ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) )
70	69 4	wal	⊢ ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) )
71	70 52	wal	⊢ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) )
72	60	csn	⊢ { ⟨ 𝑚 , 𝑒 ⟩ }
73	48 72	cima	⊢ ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } )
74		cmesy	⊢ mESyn
75	6 74	cfv	⊢ ( mESyn ‘ 𝑡 )
76	54 75	cfv	⊢ ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 )
77	42 76	cop	⊢ ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩
78	77	csn	⊢ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ }
79	48 78	cima	⊢ ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } )
80	54 10	cfv	⊢ ( 1st ‘ 𝑒 )
81	80	csn	⊢ { ( 1st ‘ 𝑒 ) }
82	9 81	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } )
83	79 82	cin	⊢ ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
84	73 83	wceq	⊢ ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
85	84 52 35	wral	⊢ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
86	51 71 85	w3a	⊢ ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) )
87	86 38 33	wral	⊢ ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) )
88	87 30 37	crio	⊢ ( ℩ 𝑛 ∈ ( ( mUV ‘ 𝑡 ) ↑pm ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) ) ) ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) )
89	3 29 88	cmpt	⊢ ( 𝑓 ∈ X 𝑎 ∈ ( mSA ‘ 𝑡 ) ( ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } ) ↑m X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ) ↦ ( ℩ 𝑛 ∈ ( ( mUV ‘ 𝑡 ) ↑pm ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) ) ) ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) ) )
90	1 2 89	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑓 ∈ X 𝑎 ∈ ( mSA ‘ 𝑡 ) ( ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } ) ↑m X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ) ↦ ( ℩ 𝑛 ∈ ( ( mUV ‘ 𝑡 ) ↑pm ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) ) ) ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) ) ) )
91	0 90	wceq	⊢ mFromItp = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ X 𝑎 ∈ ( mSA ‘ 𝑡 ) ( ( ( mUV ‘ 𝑡 ) “ { ( ( 1st ‘ 𝑡 ) ‘ 𝑎 ) } ) ↑m X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ) ↦ ( ℩ 𝑛 ∈ ( ( mUV ‘ 𝑡 ) ↑pm ( ( mVL ‘ 𝑡 ) × ( mEx ‘ 𝑡 ) ) ) ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( ∀ 𝑣 ∈ ( mVR ‘ 𝑡 ) ⟨ 𝑚 , ( ( mVH ‘ 𝑡 ) ‘ 𝑣 ) ⟩ 𝑛 ( 𝑚 ‘ 𝑣 ) ∧ ∀ 𝑒 ∀ 𝑎 ∀ 𝑔 ( 𝑒 ( mST ‘ 𝑡 ) ⟨ 𝑎 , 𝑔 ⟩ → ⟨ 𝑚 , 𝑒 ⟩ 𝑛 ( 𝑓 ‘ ( 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ↦ ( 𝑚 𝑛 ( 𝑔 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑖 ) ) ) ) ) ) ∧ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( 𝑛 “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( 𝑛 “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) ) ) )