![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-conn | Structured version Visualization version GIF version |
Description: Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.) |
Ref | Expression |
---|---|
df-conn | ⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cconn 22785 | . 2 class Conn | |
2 | vj | . . . . . 6 setvar 𝑗 | |
3 | 2 | cv 1541 | . . . . 5 class 𝑗 |
4 | ccld 22390 | . . . . . 6 class Clsd | |
5 | 3, 4 | cfv 6500 | . . . . 5 class (Clsd‘𝑗) |
6 | 3, 5 | cin 3913 | . . . 4 class (𝑗 ∩ (Clsd‘𝑗)) |
7 | c0 4286 | . . . . 5 class ∅ | |
8 | 3 | cuni 4869 | . . . . 5 class ∪ 𝑗 |
9 | 7, 8 | cpr 4592 | . . . 4 class {∅, ∪ 𝑗} |
10 | 6, 9 | wceq 1542 | . . 3 wff (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗} |
11 | ctop 22265 | . . 3 class Top | |
12 | 10, 2, 11 | crab 3406 | . 2 class {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |
13 | 1, 12 | wceq 1542 | 1 wff Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} |
Colors of variables: wff setvar class |
This definition is referenced by: isconn 22787 |
Copyright terms: Public domain | W3C validator |