Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mfitp Structured version   Visualization version   GIF version

Definition df-mfitp 32770
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
StepHypRef Expression
1 cmfitp 32759 . 2 class mFromItp
2 vt . . 3 setvar 𝑡
3 cvv 3492 . . 3 class V
4 vf . . . 4 setvar 𝑓
5 va . . . . 5 setvar 𝑎
62cv 1527 . . . . . 6 class 𝑡
7 cmsa 32730 . . . . . 6 class mSA
86, 7cfv 6348 . . . . 5 class (mSA‘𝑡)
9 cmuv 32749 . . . . . . . 8 class mUV
106, 9cfv 6348 . . . . . . 7 class (mUV‘𝑡)
115cv 1527 . . . . . . . . 9 class 𝑎
12 c1st 7676 . . . . . . . . . 10 class 1st
136, 12cfv 6348 . . . . . . . . 9 class (1st𝑡)
1411, 13cfv 6348 . . . . . . . 8 class ((1st𝑡)‘𝑎)
1514csn 4557 . . . . . . 7 class {((1st𝑡)‘𝑎)}
1610, 15cima 5551 . . . . . 6 class ((mUV‘𝑡) “ {((1st𝑡)‘𝑎)})
17 vi . . . . . . 7 setvar 𝑖
18 cmvrs 32613 . . . . . . . . 9 class mVars
196, 18cfv 6348 . . . . . . . 8 class (mVars‘𝑡)
2011, 19cfv 6348 . . . . . . 7 class ((mVars‘𝑡)‘𝑎)
2117cv 1527 . . . . . . . . . 10 class 𝑖
22 cmty 32606 . . . . . . . . . . 11 class mType
236, 22cfv 6348 . . . . . . . . . 10 class (mType‘𝑡)
2421, 23cfv 6348 . . . . . . . . 9 class ((mType‘𝑡)‘𝑖)
2524csn 4557 . . . . . . . 8 class {((mType‘𝑡)‘𝑖)}
2610, 25cima 5551 . . . . . . 7 class ((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
2717, 20, 26cixp 8449 . . . . . 6 class X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
28 cmap 8395 . . . . . 6 class m
2916, 27, 28co 7145 . . . . 5 class (((mUV‘𝑡) “ {((1st𝑡)‘𝑎)}) ↑m X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}))
305, 8, 29cixp 8449 . . . 4 class X𝑎 ∈ (mSA‘𝑡)(((mUV‘𝑡) “ {((1st𝑡)‘𝑎)}) ↑m X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}))
31 vm . . . . . . . . . . 11 setvar 𝑚
3231cv 1527 . . . . . . . . . 10 class 𝑚
33 vv . . . . . . . . . . . 12 setvar 𝑣
3433cv 1527 . . . . . . . . . . 11 class 𝑣
35 cmvh 32616 . . . . . . . . . . . 12 class mVH
366, 35cfv 6348 . . . . . . . . . . 11 class (mVH‘𝑡)
3734, 36cfv 6348 . . . . . . . . . 10 class ((mVH‘𝑡)‘𝑣)
3832, 37cop 4563 . . . . . . . . 9 class 𝑚, ((mVH‘𝑡)‘𝑣)⟩
3934, 32cfv 6348 . . . . . . . . 9 class (𝑚𝑣)
40 vn . . . . . . . . . 10 setvar 𝑛
4140cv 1527 . . . . . . . . 9 class 𝑛
4238, 39, 41wbr 5057 . . . . . . . 8 wff 𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣)
43 cmvar 32605 . . . . . . . . 9 class mVR
446, 43cfv 6348 . . . . . . . 8 class (mVR‘𝑡)
4542, 33, 44wral 3135 . . . . . . 7 wff 𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣)
46 ve . . . . . . . . . . . . 13 setvar 𝑒
4746cv 1527 . . . . . . . . . . . 12 class 𝑒
48 vg . . . . . . . . . . . . . 14 setvar 𝑔
4948cv 1527 . . . . . . . . . . . . 13 class 𝑔
5011, 49cop 4563 . . . . . . . . . . . 12 class 𝑎, 𝑔
51 cmst 32736 . . . . . . . . . . . . 13 class mST
526, 51cfv 6348 . . . . . . . . . . . 12 class (mST‘𝑡)
5347, 50, 52wbr 5057 . . . . . . . . . . 11 wff 𝑒(mST‘𝑡)⟨𝑎, 𝑔
5432, 47cop 4563 . . . . . . . . . . . 12 class 𝑚, 𝑒
5521, 36cfv 6348 . . . . . . . . . . . . . . . 16 class ((mVH‘𝑡)‘𝑖)
5655, 49cfv 6348 . . . . . . . . . . . . . . 15 class (𝑔‘((mVH‘𝑡)‘𝑖))
5732, 56, 41co 7145 . . . . . . . . . . . . . 14 class (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))
5817, 20, 57cmpt 5137 . . . . . . . . . . . . 13 class (𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))
594cv 1527 . . . . . . . . . . . . 13 class 𝑓
6058, 59cfv 6348 . . . . . . . . . . . 12 class (𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))
6154, 60, 41wbr 5057 . . . . . . . . . . 11 wff 𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))
6253, 61wi 4 . . . . . . . . . 10 wff (𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6362, 48wal 1526 . . . . . . . . 9 wff 𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6463, 5wal 1526 . . . . . . . 8 wff 𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6564, 46wal 1526 . . . . . . 7 wff 𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6654csn 4557 . . . . . . . . . 10 class {⟨𝑚, 𝑒⟩}
6741, 66cima 5551 . . . . . . . . 9 class (𝑛 “ {⟨𝑚, 𝑒⟩})
68 cmesy 32733 . . . . . . . . . . . . . . 15 class mESyn
696, 68cfv 6348 . . . . . . . . . . . . . 14 class (mESyn‘𝑡)
7047, 69cfv 6348 . . . . . . . . . . . . 13 class ((mESyn‘𝑡)‘𝑒)
7132, 70cop 4563 . . . . . . . . . . . 12 class 𝑚, ((mESyn‘𝑡)‘𝑒)⟩
7271csn 4557 . . . . . . . . . . 11 class {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}
7341, 72cima 5551 . . . . . . . . . 10 class (𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩})
7447, 12cfv 6348 . . . . . . . . . . . 12 class (1st𝑒)
7574csn 4557 . . . . . . . . . . 11 class {(1st𝑒)}
7610, 75cima 5551 . . . . . . . . . 10 class ((mUV‘𝑡) “ {(1st𝑒)})
7773, 76cin 3932 . . . . . . . . 9 class ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))
7867, 77wceq 1528 . . . . . . . 8 wff (𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))
79 cmex 32611 . . . . . . . . 9 class mEx
806, 79cfv 6348 . . . . . . . 8 class (mEx‘𝑡)
8178, 46, 80wral 3135 . . . . . . 7 wff 𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))
8245, 65, 81w3a 1079 . . . . . 6 wff (∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣) ∧ ∀𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)})))
83 cmvl 32750 . . . . . . 7 class mVL
846, 83cfv 6348 . . . . . 6 class (mVL‘𝑡)
8582, 31, 84wral 3135 . . . . 5 wff 𝑚 ∈ (mVL‘𝑡)(∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣) ∧ ∀𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)})))
8684, 80cxp 5546 . . . . . 6 class ((mVL‘𝑡) × (mEx‘𝑡))
87 cpm 8396 . . . . . 6 class pm
8810, 86, 87co 7145 . . . . 5 class ((mUV‘𝑡) ↑pm ((mVL‘𝑡) × (mEx‘𝑡)))
8985, 40, 88crio 7102 . . . 4 class (𝑛 ∈ ((mUV‘𝑡) ↑pm ((mVL‘𝑡) × (mEx‘𝑡)))∀𝑚 ∈ (mVL‘𝑡)(∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣) ∧ ∀𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))))
904, 30, 89cmpt 5137 . . 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𝑒)})))))
912, 3, 90cmpt 5137 . 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𝑒)}))))))
921, 91wceq 1528 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𝑒)}))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator