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 33104
 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 33093 . 2 class mFromItp
2 vt . . 3 setvar 𝑡
3 cvv 3409 . . 3 class V
4 vf . . . 4 setvar 𝑓
5 va . . . . 5 setvar 𝑎
62cv 1537 . . . . . 6 class 𝑡
7 cmsa 33064 . . . . . 6 class mSA
86, 7cfv 6335 . . . . 5 class (mSA‘𝑡)
9 cmuv 33083 . . . . . . . 8 class mUV
106, 9cfv 6335 . . . . . . 7 class (mUV‘𝑡)
115cv 1537 . . . . . . . . 9 class 𝑎
12 c1st 7691 . . . . . . . . . 10 class 1st
136, 12cfv 6335 . . . . . . . . 9 class (1st𝑡)
1411, 13cfv 6335 . . . . . . . 8 class ((1st𝑡)‘𝑎)
1514csn 4522 . . . . . . 7 class {((1st𝑡)‘𝑎)}
1610, 15cima 5527 . . . . . 6 class ((mUV‘𝑡) “ {((1st𝑡)‘𝑎)})
17 vi . . . . . . 7 setvar 𝑖
18 cmvrs 32947 . . . . . . . . 9 class mVars
196, 18cfv 6335 . . . . . . . 8 class (mVars‘𝑡)
2011, 19cfv 6335 . . . . . . 7 class ((mVars‘𝑡)‘𝑎)
2117cv 1537 . . . . . . . . . 10 class 𝑖
22 cmty 32940 . . . . . . . . . . 11 class mType
236, 22cfv 6335 . . . . . . . . . 10 class (mType‘𝑡)
2421, 23cfv 6335 . . . . . . . . 9 class ((mType‘𝑡)‘𝑖)
2524csn 4522 . . . . . . . 8 class {((mType‘𝑡)‘𝑖)}
2610, 25cima 5527 . . . . . . 7 class ((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
2717, 20, 26cixp 8479 . . . . . 6 class X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
28 cmap 8416 . . . . . 6 class m
2916, 27, 28co 7150 . . . . 5 class (((mUV‘𝑡) “ {((1st𝑡)‘𝑎)}) ↑m X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}))
305, 8, 29cixp 8479 . . . 4 class X𝑎 ∈ (mSA‘𝑡)(((mUV‘𝑡) “ {((1st𝑡)‘𝑎)}) ↑m X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}))
31 vm . . . . . . . . . . 11 setvar 𝑚
3231cv 1537 . . . . . . . . . 10 class 𝑚
33 vv . . . . . . . . . . . 12 setvar 𝑣
3433cv 1537 . . . . . . . . . . 11 class 𝑣
35 cmvh 32950 . . . . . . . . . . . 12 class mVH
366, 35cfv 6335 . . . . . . . . . . 11 class (mVH‘𝑡)
3734, 36cfv 6335 . . . . . . . . . 10 class ((mVH‘𝑡)‘𝑣)
3832, 37cop 4528 . . . . . . . . 9 class 𝑚, ((mVH‘𝑡)‘𝑣)⟩
3934, 32cfv 6335 . . . . . . . . 9 class (𝑚𝑣)
40 vn . . . . . . . . . 10 setvar 𝑛
4140cv 1537 . . . . . . . . 9 class 𝑛
4238, 39, 41wbr 5032 . . . . . . . 8 wff 𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣)
43 cmvar 32939 . . . . . . . . 9 class mVR
446, 43cfv 6335 . . . . . . . 8 class (mVR‘𝑡)
4542, 33, 44wral 3070 . . . . . . 7 wff 𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣)
46 ve . . . . . . . . . . . . 13 setvar 𝑒
4746cv 1537 . . . . . . . . . . . 12 class 𝑒
48 vg . . . . . . . . . . . . . 14 setvar 𝑔
4948cv 1537 . . . . . . . . . . . . 13 class 𝑔
5011, 49cop 4528 . . . . . . . . . . . 12 class 𝑎, 𝑔
51 cmst 33070 . . . . . . . . . . . . 13 class mST
526, 51cfv 6335 . . . . . . . . . . . 12 class (mST‘𝑡)
5347, 50, 52wbr 5032 . . . . . . . . . . 11 wff 𝑒(mST‘𝑡)⟨𝑎, 𝑔
5432, 47cop 4528 . . . . . . . . . . . 12 class 𝑚, 𝑒
5521, 36cfv 6335 . . . . . . . . . . . . . . . 16 class ((mVH‘𝑡)‘𝑖)
5655, 49cfv 6335 . . . . . . . . . . . . . . 15 class (𝑔‘((mVH‘𝑡)‘𝑖))
5732, 56, 41co 7150 . . . . . . . . . . . . . 14 class (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))
5817, 20, 57cmpt 5112 . . . . . . . . . . . . 13 class (𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))
594cv 1537 . . . . . . . . . . . . 13 class 𝑓
6058, 59cfv 6335 . . . . . . . . . . . 12 class (𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))
6154, 60, 41wbr 5032 . . . . . . . . . . 11 wff 𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))
6253, 61wi 4 . . . . . . . . . 10 wff (𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6362, 48wal 1536 . . . . . . . . 9 wff 𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6463, 5wal 1536 . . . . . . . 8 wff 𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6564, 46wal 1536 . . . . . . 7 wff 𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖))))))
6654csn 4522 . . . . . . . . . 10 class {⟨𝑚, 𝑒⟩}
6741, 66cima 5527 . . . . . . . . 9 class (𝑛 “ {⟨𝑚, 𝑒⟩})
68 cmesy 33067 . . . . . . . . . . . . . . 15 class mESyn
696, 68cfv 6335 . . . . . . . . . . . . . 14 class (mESyn‘𝑡)
7047, 69cfv 6335 . . . . . . . . . . . . 13 class ((mESyn‘𝑡)‘𝑒)
7132, 70cop 4528 . . . . . . . . . . . 12 class 𝑚, ((mESyn‘𝑡)‘𝑒)⟩
7271csn 4522 . . . . . . . . . . 11 class {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}
7341, 72cima 5527 . . . . . . . . . 10 class (𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩})
7447, 12cfv 6335 . . . . . . . . . . . 12 class (1st𝑒)
7574csn 4522 . . . . . . . . . . 11 class {(1st𝑒)}
7610, 75cima 5527 . . . . . . . . . 10 class ((mUV‘𝑡) “ {(1st𝑒)})
7773, 76cin 3857 . . . . . . . . 9 class ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))
7867, 77wceq 1538 . . . . . . . 8 wff (𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))
79 cmex 32945 . . . . . . . . 9 class mEx
806, 79cfv 6335 . . . . . . . 8 class (mEx‘𝑡)
8178, 46, 80wral 3070 . . . . . . 7 wff 𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))
8245, 65, 81w3a 1084 . . . . . 6 wff (∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣) ∧ ∀𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)})))
83 cmvl 33084 . . . . . . 7 class mVL
846, 83cfv 6335 . . . . . 6 class (mVL‘𝑡)
8582, 31, 84wral 3070 . . . . 5 wff 𝑚 ∈ (mVL‘𝑡)(∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣) ∧ ∀𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)})))
8684, 80cxp 5522 . . . . . 6 class ((mVL‘𝑡) × (mEx‘𝑡))
87 cpm 8417 . . . . . 6 class pm
8810, 86, 87co 7150 . . . . 5 class ((mUV‘𝑡) ↑pm ((mVL‘𝑡) × (mEx‘𝑡)))
8985, 40, 88crio 7107 . . . 4 class (𝑛 ∈ ((mUV‘𝑡) ↑pm ((mVL‘𝑡) × (mEx‘𝑡)))∀𝑚 ∈ (mVL‘𝑡)(∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚𝑣) ∧ ∀𝑒𝑎𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st𝑒)}))))
904, 30, 89cmpt 5112 . . 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 5112 . 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 1538 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