Definition df-mfitp 35572

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

Distinct variable group:   𝑒,𝑎,𝑓,𝑔,𝑖,𝑚,𝑛,𝑡,𝑣

Detailed syntax breakdown of Definition df-mfitp

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

This definition is referenced by: (None)