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 34612
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 34601 . 2 class mFromItp
2 vt . . 3 setvar 𝑑
3 cvv 3474 . . 3 class V
4 vf . . . 4 setvar 𝑓
5 va . . . . 5 setvar π‘Ž
62cv 1540 . . . . . 6 class 𝑑
7 cmsa 34572 . . . . . 6 class mSA
86, 7cfv 6543 . . . . 5 class (mSAβ€˜π‘‘)
9 cmuv 34591 . . . . . . . 8 class mUV
106, 9cfv 6543 . . . . . . 7 class (mUVβ€˜π‘‘)
115cv 1540 . . . . . . . . 9 class π‘Ž
12 c1st 7972 . . . . . . . . . 10 class 1st
136, 12cfv 6543 . . . . . . . . 9 class (1st β€˜π‘‘)
1411, 13cfv 6543 . . . . . . . 8 class ((1st β€˜π‘‘)β€˜π‘Ž)
1514csn 4628 . . . . . . 7 class {((1st β€˜π‘‘)β€˜π‘Ž)}
1610, 15cima 5679 . . . . . 6 class ((mUVβ€˜π‘‘) β€œ {((1st β€˜π‘‘)β€˜π‘Ž)})
17 vi . . . . . . 7 setvar 𝑖
18 cmvrs 34455 . . . . . . . . 9 class mVars
196, 18cfv 6543 . . . . . . . 8 class (mVarsβ€˜π‘‘)
2011, 19cfv 6543 . . . . . . 7 class ((mVarsβ€˜π‘‘)β€˜π‘Ž)
2117cv 1540 . . . . . . . . . 10 class 𝑖
22 cmty 34448 . . . . . . . . . . 11 class mType
236, 22cfv 6543 . . . . . . . . . 10 class (mTypeβ€˜π‘‘)
2421, 23cfv 6543 . . . . . . . . 9 class ((mTypeβ€˜π‘‘)β€˜π‘–)
2524csn 4628 . . . . . . . 8 class {((mTypeβ€˜π‘‘)β€˜π‘–)}
2610, 25cima 5679 . . . . . . 7 class ((mUVβ€˜π‘‘) β€œ {((mTypeβ€˜π‘‘)β€˜π‘–)})
2717, 20, 26cixp 8890 . . . . . 6 class X𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž)((mUVβ€˜π‘‘) β€œ {((mTypeβ€˜π‘‘)β€˜π‘–)})
28 cmap 8819 . . . . . 6 class ↑m
2916, 27, 28co 7408 . . . . 5 class (((mUVβ€˜π‘‘) β€œ {((1st β€˜π‘‘)β€˜π‘Ž)}) ↑m X𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž)((mUVβ€˜π‘‘) β€œ {((mTypeβ€˜π‘‘)β€˜π‘–)}))
305, 8, 29cixp 8890 . . . 4 class Xπ‘Ž ∈ (mSAβ€˜π‘‘)(((mUVβ€˜π‘‘) β€œ {((1st β€˜π‘‘)β€˜π‘Ž)}) ↑m X𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž)((mUVβ€˜π‘‘) β€œ {((mTypeβ€˜π‘‘)β€˜π‘–)}))
31 vm . . . . . . . . . . 11 setvar π‘š
3231cv 1540 . . . . . . . . . 10 class π‘š
33 vv . . . . . . . . . . . 12 setvar 𝑣
3433cv 1540 . . . . . . . . . . 11 class 𝑣
35 cmvh 34458 . . . . . . . . . . . 12 class mVH
366, 35cfv 6543 . . . . . . . . . . 11 class (mVHβ€˜π‘‘)
3734, 36cfv 6543 . . . . . . . . . 10 class ((mVHβ€˜π‘‘)β€˜π‘£)
3832, 37cop 4634 . . . . . . . . 9 class βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘£)⟩
3934, 32cfv 6543 . . . . . . . . 9 class (π‘šβ€˜π‘£)
40 vn . . . . . . . . . 10 setvar 𝑛
4140cv 1540 . . . . . . . . 9 class 𝑛
4238, 39, 41wbr 5148 . . . . . . . 8 wff βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘£)βŸ©π‘›(π‘šβ€˜π‘£)
43 cmvar 34447 . . . . . . . . 9 class mVR
446, 43cfv 6543 . . . . . . . 8 class (mVRβ€˜π‘‘)
4542, 33, 44wral 3061 . . . . . . 7 wff βˆ€π‘£ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘£)βŸ©π‘›(π‘šβ€˜π‘£)
46 ve . . . . . . . . . . . . 13 setvar 𝑒
4746cv 1540 . . . . . . . . . . . 12 class 𝑒
48 vg . . . . . . . . . . . . . 14 setvar 𝑔
4948cv 1540 . . . . . . . . . . . . 13 class 𝑔
5011, 49cop 4634 . . . . . . . . . . . 12 class βŸ¨π‘Ž, π‘”βŸ©
51 cmst 34578 . . . . . . . . . . . . 13 class mST
526, 51cfv 6543 . . . . . . . . . . . 12 class (mSTβ€˜π‘‘)
5347, 50, 52wbr 5148 . . . . . . . . . . 11 wff 𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ©
5432, 47cop 4634 . . . . . . . . . . . 12 class βŸ¨π‘š, π‘’βŸ©
5521, 36cfv 6543 . . . . . . . . . . . . . . . 16 class ((mVHβ€˜π‘‘)β€˜π‘–)
5655, 49cfv 6543 . . . . . . . . . . . . . . 15 class (π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–))
5732, 56, 41co 7408 . . . . . . . . . . . . . 14 class (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–)))
5817, 20, 57cmpt 5231 . . . . . . . . . . . . 13 class (𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–))))
594cv 1540 . . . . . . . . . . . . 13 class 𝑓
6058, 59cfv 6543 . . . . . . . . . . . 12 class (π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–)))))
6154, 60, 41wbr 5148 . . . . . . . . . . 11 wff βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–)))))
6253, 61wi 4 . . . . . . . . . 10 wff (𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–))))))
6362, 48wal 1539 . . . . . . . . 9 wff βˆ€π‘”(𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–))))))
6463, 5wal 1539 . . . . . . . 8 wff βˆ€π‘Žβˆ€π‘”(𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–))))))
6564, 46wal 1539 . . . . . . 7 wff βˆ€π‘’βˆ€π‘Žβˆ€π‘”(𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–))))))
6654csn 4628 . . . . . . . . . 10 class {βŸ¨π‘š, π‘’βŸ©}
6741, 66cima 5679 . . . . . . . . 9 class (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©})
68 cmesy 34575 . . . . . . . . . . . . . . 15 class mESyn
696, 68cfv 6543 . . . . . . . . . . . . . 14 class (mESynβ€˜π‘‘)
7047, 69cfv 6543 . . . . . . . . . . . . 13 class ((mESynβ€˜π‘‘)β€˜π‘’)
7132, 70cop 4634 . . . . . . . . . . . 12 class βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩
7271csn 4628 . . . . . . . . . . 11 class {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}
7341, 72cima 5679 . . . . . . . . . 10 class (𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩})
7447, 12cfv 6543 . . . . . . . . . . . 12 class (1st β€˜π‘’)
7574csn 4628 . . . . . . . . . . 11 class {(1st β€˜π‘’)}
7610, 75cima 5679 . . . . . . . . . 10 class ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})
7773, 76cin 3947 . . . . . . . . 9 class ((𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
7867, 77wceq 1541 . . . . . . . 8 wff (𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = ((𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
79 cmex 34453 . . . . . . . . 9 class mEx
806, 79cfv 6543 . . . . . . . 8 class (mExβ€˜π‘‘)
8178, 46, 80wral 3061 . . . . . . 7 wff βˆ€π‘’ ∈ (mExβ€˜π‘‘)(𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = ((𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
8245, 65, 81w3a 1087 . . . . . 6 wff (βˆ€π‘£ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘£)βŸ©π‘›(π‘šβ€˜π‘£) ∧ βˆ€π‘’βˆ€π‘Žβˆ€π‘”(𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–)))))) ∧ βˆ€π‘’ ∈ (mExβ€˜π‘‘)(𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = ((𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})))
83 cmvl 34592 . . . . . . 7 class mVL
846, 83cfv 6543 . . . . . 6 class (mVLβ€˜π‘‘)
8582, 31, 84wral 3061 . . . . 5 wff βˆ€π‘š ∈ (mVLβ€˜π‘‘)(βˆ€π‘£ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘£)βŸ©π‘›(π‘šβ€˜π‘£) ∧ βˆ€π‘’βˆ€π‘Žβˆ€π‘”(𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–)))))) ∧ βˆ€π‘’ ∈ (mExβ€˜π‘‘)(𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = ((𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})))
8684, 80cxp 5674 . . . . . 6 class ((mVLβ€˜π‘‘) Γ— (mExβ€˜π‘‘))
87 cpm 8820 . . . . . 6 class ↑pm
8810, 86, 87co 7408 . . . . 5 class ((mUVβ€˜π‘‘) ↑pm ((mVLβ€˜π‘‘) Γ— (mExβ€˜π‘‘)))
8985, 40, 88crio 7363 . . . 4 class (℩𝑛 ∈ ((mUVβ€˜π‘‘) ↑pm ((mVLβ€˜π‘‘) Γ— (mExβ€˜π‘‘)))βˆ€π‘š ∈ (mVLβ€˜π‘‘)(βˆ€π‘£ ∈ (mVRβ€˜π‘‘)βŸ¨π‘š, ((mVHβ€˜π‘‘)β€˜π‘£)βŸ©π‘›(π‘šβ€˜π‘£) ∧ βˆ€π‘’βˆ€π‘Žβˆ€π‘”(𝑒(mSTβ€˜π‘‘)βŸ¨π‘Ž, π‘”βŸ© β†’ βŸ¨π‘š, π‘’βŸ©π‘›(π‘“β€˜(𝑖 ∈ ((mVarsβ€˜π‘‘)β€˜π‘Ž) ↦ (π‘šπ‘›(π‘”β€˜((mVHβ€˜π‘‘)β€˜π‘–)))))) ∧ βˆ€π‘’ ∈ (mExβ€˜π‘‘)(𝑛 β€œ {βŸ¨π‘š, π‘’βŸ©}) = ((𝑛 β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))))
904, 30, 89cmpt 5231 . . 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 5231 . 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 1541 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