Detailed syntax breakdown of Definition df-cls
Step | Hyp | Ref
| Expression |
1 | | ccl 12494 |
. 2
class
cls |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | ctop 12395 |
. . 3
class
Top |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | 2 | cv 1334 |
. . . . . 6
class 𝑗 |
6 | 5 | cuni 3772 |
. . . . 5
class ∪ 𝑗 |
7 | 6 | cpw 3543 |
. . . 4
class 𝒫
∪ 𝑗 |
8 | 4 | cv 1334 |
. . . . . . 7
class 𝑥 |
9 | | vy |
. . . . . . . 8
setvar 𝑦 |
10 | 9 | cv 1334 |
. . . . . . 7
class 𝑦 |
11 | 8, 10 | wss 3102 |
. . . . . 6
wff 𝑥 ⊆ 𝑦 |
12 | | ccld 12492 |
. . . . . . 7
class
Clsd |
13 | 5, 12 | cfv 5170 |
. . . . . 6
class
(Clsd‘𝑗) |
14 | 11, 9, 13 | crab 2439 |
. . . . 5
class {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦} |
15 | 14 | cint 3807 |
. . . 4
class ∩ {𝑦
∈ (Clsd‘𝑗)
∣ 𝑥 ⊆ 𝑦} |
16 | 4, 7, 15 | cmpt 4025 |
. . 3
class (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}) |
17 | 2, 3, 16 | cmpt 4025 |
. 2
class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |
18 | 1, 17 | wceq 1335 |
1
wff cls =
(𝑗 ∈ Top ↦
(𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |