Detailed syntax breakdown of Definition df-mpps
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cmpps 33340 |
. 2
class
mPPSt |
| 2 | | vt |
. . 3
setvar 𝑡 |
| 3 | | cvv 3422 |
. . 3
class
V |
| 4 | | vd |
. . . . . . . 8
setvar 𝑑 |
| 5 | 4 | cv 1538 |
. . . . . . 7
class 𝑑 |
| 6 | | vh |
. . . . . . . 8
setvar ℎ |
| 7 | 6 | cv 1538 |
. . . . . . 7
class ℎ |
| 8 | | va |
. . . . . . . 8
setvar 𝑎 |
| 9 | 8 | cv 1538 |
. . . . . . 7
class 𝑎 |
| 10 | 5, 7, 9 | cotp 4566 |
. . . . . 6
class
⟨𝑑, ℎ, 𝑎⟩ |
| 11 | 2 | cv 1538 |
. . . . . . 7
class 𝑡 |
| 12 | | cmpst 33335 |
. . . . . . 7
class
mPreSt |
| 13 | 11, 12 | cfv 6418 |
. . . . . 6
class
(mPreSt‘𝑡) |
| 14 | 10, 13 | wcel 2108 |
. . . . 5
wff ⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) |
| 15 | | cmcls 33339 |
. . . . . . . 8
class
mCls |
| 16 | 11, 15 | cfv 6418 |
. . . . . . 7
class
(mCls‘𝑡) |
| 17 | 5, 7, 16 | co 7255 |
. . . . . 6
class (𝑑(mCls‘𝑡)ℎ) |
| 18 | 9, 17 | wcel 2108 |
. . . . 5
wff 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ) |
| 19 | 14, 18 | wa 395 |
. . . 4
wff
(⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ)) |
| 20 | 19, 4, 6, 8 | coprab 7256 |
. . 3
class
{⟨⟨𝑑,
ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))} |
| 21 | 2, 3, 20 | cmpt 5153 |
. 2
class (𝑡 ∈ V ↦
{⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) |
| 22 | 1, 21 | wceq 1539 |
1
wff mPPSt =
(𝑡 ∈ V ↦
{⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}) |
