Detailed syntax breakdown of Definition df-cls
| Step | Hyp | Ref
| Expression |
| 1 | | ccl 23026 |
. 2
class
cls |
| 2 | | vj |
. . 3
setvar 𝑗 |
| 3 | | ctop 22899 |
. . 3
class
Top |
| 4 | | vx |
. . . 4
setvar 𝑥 |
| 5 | 2 | cv 1539 |
. . . . . 6
class 𝑗 |
| 6 | 5 | cuni 4907 |
. . . . 5
class ∪ 𝑗 |
| 7 | 6 | cpw 4600 |
. . . 4
class 𝒫
∪ 𝑗 |
| 8 | 4 | cv 1539 |
. . . . . . 7
class 𝑥 |
| 9 | | vy |
. . . . . . . 8
setvar 𝑦 |
| 10 | 9 | cv 1539 |
. . . . . . 7
class 𝑦 |
| 11 | 8, 10 | wss 3951 |
. . . . . 6
wff 𝑥 ⊆ 𝑦 |
| 12 | | ccld 23024 |
. . . . . . 7
class
Clsd |
| 13 | 5, 12 | cfv 6561 |
. . . . . 6
class
(Clsd‘𝑗) |
| 14 | 11, 9, 13 | crab 3436 |
. . . . 5
class {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦} |
| 15 | 14 | cint 4946 |
. . . 4
class ∩ {𝑦
∈ (Clsd‘𝑗)
∣ 𝑥 ⊆ 𝑦} |
| 16 | 4, 7, 15 | cmpt 5225 |
. . 3
class (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}) |
| 17 | 2, 3, 16 | cmpt 5225 |
. 2
class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |
| 18 | 1, 17 | wceq 1540 |
1
wff cls =
(𝑗 ∈ Top ↦
(𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |