Detailed syntax breakdown of Definition df-conn
Step | Hyp | Ref
| Expression |
1 | | cconn 23406 |
. 2
class
Conn |
2 | | vj |
. . . . . 6
setvar 𝑗 |
3 | 2 | cv 1533 |
. . . . 5
class 𝑗 |
4 | | ccld 23011 |
. . . . . 6
class
Clsd |
5 | 3, 4 | cfv 6554 |
. . . . 5
class
(Clsd‘𝑗) |
6 | 3, 5 | cin 3946 |
. . . 4
class (𝑗 ∩ (Clsd‘𝑗)) |
7 | | c0 4325 |
. . . . 5
class
∅ |
8 | 3 | cuni 4913 |
. . . . 5
class ∪ 𝑗 |
9 | 7, 8 | cpr 4635 |
. . . 4
class {∅,
∪ 𝑗} |
10 | 6, 9 | wceq 1534 |
. . 3
wff (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗} |
11 | | ctop 22886 |
. . 3
class
Top |
12 | 10, 2, 11 | crab 3419 |
. 2
class {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |
13 | 1, 12 | wceq 1534 |
1
wff Conn =
{𝑗 ∈ Top ∣
(𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |