Detailed syntax breakdown of Definition df-pmtr
Step | Hyp | Ref
| Expression |
1 | | cpmtr 18993 |
. 2
class
pmTrsp |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cvv 3427 |
. . 3
class
V |
4 | | vp |
. . . 4
setvar 𝑝 |
5 | | vy |
. . . . . . 7
setvar 𝑦 |
6 | 5 | cv 1538 |
. . . . . 6
class 𝑦 |
7 | | c2o 8266 |
. . . . . 6
class
2o |
8 | | cen 8693 |
. . . . . 6
class
≈ |
9 | 6, 7, 8 | wbr 5075 |
. . . . 5
wff 𝑦 ≈
2o |
10 | 2 | cv 1538 |
. . . . . 6
class 𝑑 |
11 | 10 | cpw 4535 |
. . . . 5
class 𝒫
𝑑 |
12 | 9, 5, 11 | crab 3066 |
. . . 4
class {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} |
13 | | vz |
. . . . 5
setvar 𝑧 |
14 | 13, 4 | wel 2108 |
. . . . . 6
wff 𝑧 ∈ 𝑝 |
15 | 4 | cv 1538 |
. . . . . . . 8
class 𝑝 |
16 | 13 | cv 1538 |
. . . . . . . . 9
class 𝑧 |
17 | 16 | csn 4563 |
. . . . . . . 8
class {𝑧} |
18 | 15, 17 | cdif 3885 |
. . . . . . 7
class (𝑝 ∖ {𝑧}) |
19 | 18 | cuni 4841 |
. . . . . 6
class ∪ (𝑝
∖ {𝑧}) |
20 | 14, 19, 16 | cif 4461 |
. . . . 5
class if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧) |
21 | 13, 10, 20 | cmpt 5158 |
. . . 4
class (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) |
22 | 4, 12, 21 | cmpt 5158 |
. . 3
class (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
23 | 2, 3, 22 | cmpt 5158 |
. 2
class (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
24 | 1, 23 | wceq 1539 |
1
wff pmTrsp =
(𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |