MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-conn Structured version   Visualization version   GIF version

Definition df-conn 21692
Description: Topologies are connected when only and 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.)
Assertion
Ref Expression
df-conn Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, 𝑗}}

Detailed syntax breakdown of Definition df-conn
StepHypRef Expression
1 cconn 21691 . 2 class Conn
2 vj . . . . . 6 setvar 𝑗
32cv 1519 . . . . 5 class 𝑗
4 ccld 21296 . . . . . 6 class Clsd
53, 4cfv 6217 . . . . 5 class (Clsd‘𝑗)
63, 5cin 3853 . . . 4 class (𝑗 ∩ (Clsd‘𝑗))
7 c0 4206 . . . . 5 class
83cuni 4739 . . . . 5 class 𝑗
97, 8cpr 4468 . . . 4 class {∅, 𝑗}
106, 9wceq 1520 . . 3 wff (𝑗 ∩ (Clsd‘𝑗)) = {∅, 𝑗}
11 ctop 21173 . . 3 class Top
1210, 2, 11crab 3107 . 2 class {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, 𝑗}}
131, 12wceq 1520 1 wff Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, 𝑗}}
Colors of variables: wff setvar class
This definition is referenced by:  isconn  21693
  Copyright terms: Public domain W3C validator