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 ∈ V ⟼ f ∈ ⨉ a ∈ mSA ⁡ t mUV ⁡ t 1 st ⁡ t ⁡ a ⨉ i ∈ mVars ⁡ t ⁡ a mUV ⁡ t mType ⁡ t ⁡ i ⟼ ι n ∈ mUV ⁡ t ↑ 𝑝𝑚 mVL ⁡ t × mEx ⁡ t | ∀ m ∈ mVL ⁡ t ∀ v ∈ mVR ⁡ t m mVH ⁡ t ⁡ v n m ⁡ v ∧ ∀ e ∀ a ∀ g e mST ⁡ t a g → m e n f ⁡ i ∈ mVars ⁡ t ⁡ a ⟼ m n g ⁡ mVH ⁡ t ⁡ i ∧ ∀ e ∈ mEx ⁡ t n m e = n m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e

Detailed syntax breakdown

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