Detailed syntax breakdown of Definition df-pmtr
Step | Hyp | Ref
| Expression |
1 | | cpmtr 19049 |
. 2
class
pmTrsp |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cvv 3432 |
. . 3
class
V |
4 | | vp |
. . . 4
setvar 𝑝 |
5 | | vy |
. . . . . . 7
setvar 𝑦 |
6 | 5 | cv 1538 |
. . . . . 6
class 𝑦 |
7 | | c2o 8291 |
. . . . . 6
class
2o |
8 | | cen 8730 |
. . . . . 6
class
≈ |
9 | 6, 7, 8 | wbr 5074 |
. . . . 5
wff 𝑦 ≈
2o |
10 | 2 | cv 1538 |
. . . . . 6
class 𝑑 |
11 | 10 | cpw 4533 |
. . . . 5
class 𝒫
𝑑 |
12 | 9, 5, 11 | crab 3068 |
. . . 4
class {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} |
13 | | vz |
. . . . 5
setvar 𝑧 |
14 | 13, 4 | wel 2107 |
. . . . . 6
wff 𝑧 ∈ 𝑝 |
15 | 4 | cv 1538 |
. . . . . . . 8
class 𝑝 |
16 | 13 | cv 1538 |
. . . . . . . . 9
class 𝑧 |
17 | 16 | csn 4561 |
. . . . . . . 8
class {𝑧} |
18 | 15, 17 | cdif 3884 |
. . . . . . 7
class (𝑝 ∖ {𝑧}) |
19 | 18 | cuni 4839 |
. . . . . 6
class ∪ (𝑝
∖ {𝑧}) |
20 | 14, 19, 16 | cif 4459 |
. . . . 5
class if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧) |
21 | 13, 10, 20 | cmpt 5157 |
. . . 4
class (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) |
22 | 4, 12, 21 | cmpt 5157 |
. . 3
class (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
23 | 2, 3, 22 | cmpt 5157 |
. 2
class (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
24 | 1, 23 | wceq 1539 |
1
wff pmTrsp =
(𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |