Detailed syntax breakdown of Definition df-mpps
Step | Hyp | Ref
| Expression |
1 | | cmpps 33011 |
. 2
class
mPPSt |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3398 |
. . 3
class
V |
4 | | vd |
. . . . . . . 8
setvar 𝑑 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑑 |
6 | | vh |
. . . . . . . 8
setvar ℎ |
7 | 6 | cv 1541 |
. . . . . . 7
class ℎ |
8 | | va |
. . . . . . . 8
setvar 𝑎 |
9 | 8 | cv 1541 |
. . . . . . 7
class 𝑎 |
10 | 5, 7, 9 | cotp 4524 |
. . . . . 6
class
〈𝑑, ℎ, 𝑎〉 |
11 | 2 | cv 1541 |
. . . . . . 7
class 𝑡 |
12 | | cmpst 33006 |
. . . . . . 7
class
mPreSt |
13 | 11, 12 | cfv 6339 |
. . . . . 6
class
(mPreSt‘𝑡) |
14 | 10, 13 | wcel 2114 |
. . . . 5
wff 〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) |
15 | | cmcls 33010 |
. . . . . . . 8
class
mCls |
16 | 11, 15 | cfv 6339 |
. . . . . . 7
class
(mCls‘𝑡) |
17 | 5, 7, 16 | co 7170 |
. . . . . 6
class (𝑑(mCls‘𝑡)ℎ) |
18 | 9, 17 | wcel 2114 |
. . . . 5
wff 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ) |
19 | 14, 18 | wa 399 |
. . . 4
wff
(〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ)) |
20 | 19, 4, 6, 8 | coprab 7171 |
. . 3
class
{〈〈𝑑,
ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))} |
21 | 2, 3, 20 | cmpt 5110 |
. 2
class (𝑡 ∈ V ↦
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) |
22 | 1, 21 | wceq 1542 |
1
wff mPPSt =
(𝑡 ∈ V ↦
{〈〈𝑑, ℎ〉, 𝑎〉 ∣ (〈𝑑, ℎ, 𝑎〉 ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) |