Detailed syntax breakdown of Definition df-conn
Step | Hyp | Ref
| Expression |
1 | | cconn 21214 |
. 2
class
Conn |
2 | | vj |
. . . . . 6
setvar 𝑗 |
3 | 2 | cv 1482 |
. . . . 5
class 𝑗 |
4 | | ccld 20820 |
. . . . . 6
class
Clsd |
5 | 3, 4 | cfv 5888 |
. . . . 5
class
(Clsd‘𝑗) |
6 | 3, 5 | cin 3573 |
. . . 4
class (𝑗 ∩ (Clsd‘𝑗)) |
7 | | c0 3915 |
. . . . 5
class
∅ |
8 | 3 | cuni 4436 |
. . . . 5
class ∪ 𝑗 |
9 | 7, 8 | cpr 4179 |
. . . 4
class {∅,
∪ 𝑗} |
10 | 6, 9 | wceq 1483 |
. . 3
wff (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗} |
11 | | ctop 20698 |
. . 3
class
Top |
12 | 10, 2, 11 | crab 2916 |
. 2
class {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |
13 | 1, 12 | wceq 1483 |
1
wff Conn =
{𝑗 ∈ Top ∣
(𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |