Detailed syntax breakdown of Definition df-mitp
Step | Hyp | Ref
| Expression |
1 | | cmitp 33147 |
. 2
class
mItp |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3398 |
. . 3
class
V |
4 | | va |
. . . 4
setvar 𝑎 |
5 | 2 | cv 1541 |
. . . . 5
class 𝑡 |
6 | | cmsa 33119 |
. . . . 5
class
mSA |
7 | 5, 6 | cfv 6339 |
. . . 4
class
(mSA‘𝑡) |
8 | | vg |
. . . . 5
setvar 𝑔 |
9 | | vi |
. . . . . 6
setvar 𝑖 |
10 | 4 | cv 1541 |
. . . . . . 7
class 𝑎 |
11 | | cmvrs 33002 |
. . . . . . . 8
class
mVars |
12 | 5, 11 | cfv 6339 |
. . . . . . 7
class
(mVars‘𝑡) |
13 | 10, 12 | cfv 6339 |
. . . . . 6
class
((mVars‘𝑡)‘𝑎) |
14 | | cmuv 33138 |
. . . . . . . 8
class
mUV |
15 | 5, 14 | cfv 6339 |
. . . . . . 7
class
(mUV‘𝑡) |
16 | 9 | cv 1541 |
. . . . . . . . 9
class 𝑖 |
17 | | cmty 32995 |
. . . . . . . . . 10
class
mType |
18 | 5, 17 | cfv 6339 |
. . . . . . . . 9
class
(mType‘𝑡) |
19 | 16, 18 | cfv 6339 |
. . . . . . . 8
class
((mType‘𝑡)‘𝑖) |
20 | 19 | csn 4516 |
. . . . . . 7
class
{((mType‘𝑡)‘𝑖)} |
21 | 15, 20 | cima 5528 |
. . . . . 6
class
((mUV‘𝑡)
“ {((mType‘𝑡)‘𝑖)}) |
22 | 9, 13, 21 | cixp 8507 |
. . . . 5
class X𝑖 ∈
((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) |
23 | 8 | cv 1541 |
. . . . . . . . 9
class 𝑔 |
24 | | vm |
. . . . . . . . . . 11
setvar 𝑚 |
25 | 24 | cv 1541 |
. . . . . . . . . 10
class 𝑚 |
26 | 25, 13 | cres 5527 |
. . . . . . . . 9
class (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) |
27 | 23, 26 | wceq 1542 |
. . . . . . . 8
wff 𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) |
28 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
29 | 28 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
30 | | cmevl 33143 |
. . . . . . . . . . 11
class
mEval |
31 | 5, 30 | cfv 6339 |
. . . . . . . . . 10
class
(mEval‘𝑡) |
32 | 25, 10, 31 | co 7170 |
. . . . . . . . 9
class (𝑚(mEval‘𝑡)𝑎) |
33 | 29, 32 | wceq 1542 |
. . . . . . . 8
wff 𝑥 = (𝑚(mEval‘𝑡)𝑎) |
34 | 27, 33 | wa 399 |
. . . . . . 7
wff (𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)) |
35 | | cmvl 33139 |
. . . . . . . 8
class
mVL |
36 | 5, 35 | cfv 6339 |
. . . . . . 7
class
(mVL‘𝑡) |
37 | 34, 24, 36 | wrex 3054 |
. . . . . 6
wff
∃𝑚 ∈
(mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)) |
38 | 37, 28 | cio 6295 |
. . . . 5
class
(℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))) |
39 | 8, 22, 38 | cmpt 5110 |
. . . 4
class (𝑔 ∈ X𝑖 ∈
((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))) |
40 | 4, 7, 39 | cmpt 5110 |
. . 3
class (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))) |
41 | 2, 3, 40 | cmpt 5110 |
. 2
class (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))))) |
42 | 1, 41 | wceq 1542 |
1
wff mItp =
(𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))))) |