Detailed syntax breakdown of Definition df-con
Step | Hyp | Ref
| Expression |
1 | | ccon 21024 |
. 2
class
Con |
2 | | vj |
. . . . . 6
setvar 𝑗 |
3 | 2 | cv 1474 |
. . . . 5
class 𝑗 |
4 | | ccld 20630 |
. . . . . 6
class
Clsd |
5 | 3, 4 | cfv 5804 |
. . . . 5
class
(Clsd‘𝑗) |
6 | 3, 5 | cin 3539 |
. . . 4
class (𝑗 ∩ (Clsd‘𝑗)) |
7 | | c0 3874 |
. . . . 5
class
∅ |
8 | 3 | cuni 4372 |
. . . . 5
class ∪ 𝑗 |
9 | 7, 8 | cpr 4127 |
. . . 4
class {∅,
∪ 𝑗} |
10 | 6, 9 | wceq 1475 |
. . 3
wff (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗} |
11 | | ctop 20517 |
. . 3
class
Top |
12 | 10, 2, 11 | crab 2900 |
. 2
class {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |
13 | 1, 12 | wceq 1475 |
1
wff Con =
{𝑗 ∈ Top ∣
(𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |