MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-con Unicode version

Definition df-con 17138
Description: Topologies are connected when only  (/) and  U. j are both open and closed. (Contributed by FL, 17-Nov-2008.)
Assertion
Ref Expression
df-con  |-  Con  =  { j  e.  Top  |  ( j  i^i  ( Clsd `  j ) )  =  { (/) ,  U. j } }

Detailed syntax breakdown of Definition df-con
StepHypRef Expression
1 ccon 17137 . 2  class  Con
2 vj . . . . . 6  set  j
32cv 1622 . . . . 5  class  j
4 ccld 16753 . . . . . 6  class  Clsd
53, 4cfv 5255 . . . . 5  class  ( Clsd `  j )
63, 5cin 3151 . . . 4  class  ( j  i^i  ( Clsd `  j
) )
7 c0 3455 . . . . 5  class  (/)
83cuni 3827 . . . . 5  class  U. j
97, 8cpr 3641 . . . 4  class  { (/) , 
U. j }
106, 9wceq 1623 . . 3  wff  ( j  i^i  ( Clsd `  j
) )  =  { (/)
,  U. j }
11 ctop 16631 . . 3  class  Top
1210, 2, 11crab 2547 . 2  class  { j  e.  Top  |  ( j  i^i  ( Clsd `  j ) )  =  { (/) ,  U. j } }
131, 12wceq 1623 1  wff  Con  =  { j  e.  Top  |  ( j  i^i  ( Clsd `  j ) )  =  { (/) ,  U. j } }
Colors of variables: wff set class
This definition is referenced by:  iscon  17139
  Copyright terms: Public domain W3C validator