Detailed syntax breakdown of Definition df-topsep
Step | Hyp | Ref
| Expression |
1 | | ctopsep 40741 |
. 2
class
TopSep |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1542 |
. . . . . 6
class 𝑥 |
4 | | com 7644 |
. . . . . 6
class
ω |
5 | | cdom 8624 |
. . . . . 6
class
≼ |
6 | 3, 4, 5 | wbr 5053 |
. . . . 5
wff 𝑥 ≼
ω |
7 | | vj |
. . . . . . . . 9
setvar 𝑗 |
8 | 7 | cv 1542 |
. . . . . . . 8
class 𝑗 |
9 | | ccl 21915 |
. . . . . . . 8
class
cls |
10 | 8, 9 | cfv 6380 |
. . . . . . 7
class
(cls‘𝑗) |
11 | 3, 10 | cfv 6380 |
. . . . . 6
class
((cls‘𝑗)‘𝑥) |
12 | 8 | cuni 4819 |
. . . . . 6
class ∪ 𝑗 |
13 | 11, 12 | wceq 1543 |
. . . . 5
wff
((cls‘𝑗)‘𝑥) = ∪ 𝑗 |
14 | 6, 13 | wa 399 |
. . . 4
wff (𝑥 ≼ ω ∧
((cls‘𝑗)‘𝑥) = ∪
𝑗) |
15 | 12 | cpw 4513 |
. . . 4
class 𝒫
∪ 𝑗 |
16 | 14, 2, 15 | wrex 3062 |
. . 3
wff
∃𝑥 ∈
𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗) |
17 | | ctop 21790 |
. . 3
class
Top |
18 | 16, 7, 17 | crab 3065 |
. 2
class {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)} |
19 | 1, 18 | wceq 1543 |
1
wff TopSep =
{𝑗 ∈ Top ∣
∃𝑥 ∈ 𝒫
∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)} |