Detailed syntax breakdown of Definition df-mpst
Step | Hyp | Ref
| Expression |
1 | | cmpst 33432 |
. 2
class
mPreSt |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vd |
. . . . . . . . 9
setvar 𝑑 |
5 | 4 | cv 1538 |
. . . . . . . 8
class 𝑑 |
6 | 5 | ccnv 5590 |
. . . . . . 7
class ◡𝑑 |
7 | 6, 5 | wceq 1539 |
. . . . . 6
wff ◡𝑑 = 𝑑 |
8 | 2 | cv 1538 |
. . . . . . . 8
class 𝑡 |
9 | | cmdv 33427 |
. . . . . . . 8
class
mDV |
10 | 8, 9 | cfv 6435 |
. . . . . . 7
class
(mDV‘𝑡) |
11 | 10 | cpw 4535 |
. . . . . 6
class 𝒫
(mDV‘𝑡) |
12 | 7, 4, 11 | crab 3068 |
. . . . 5
class {𝑑 ∈ 𝒫
(mDV‘𝑡) ∣ ◡𝑑 = 𝑑} |
13 | | cmex 33426 |
. . . . . . . 8
class
mEx |
14 | 8, 13 | cfv 6435 |
. . . . . . 7
class
(mEx‘𝑡) |
15 | 14 | cpw 4535 |
. . . . . 6
class 𝒫
(mEx‘𝑡) |
16 | | cfn 8731 |
. . . . . 6
class
Fin |
17 | 15, 16 | cin 3887 |
. . . . 5
class
(𝒫 (mEx‘𝑡) ∩ Fin) |
18 | 12, 17 | cxp 5589 |
. . . 4
class ({𝑑 ∈ 𝒫
(mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) |
19 | 18, 14 | cxp 5589 |
. . 3
class (({𝑑 ∈ 𝒫
(mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) ×
(mEx‘𝑡)) |
20 | 2, 3, 19 | cmpt 5159 |
. 2
class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫
(mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) ×
(mEx‘𝑡))) |
21 | 1, 20 | wceq 1539 |
1
wff mPreSt =
(𝑡 ∈ V ↦
(({𝑑 ∈ 𝒫
(mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) ×
(mEx‘𝑡))) |