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

Definition df-con 17154
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 17153 . 2  class  Con
2 vj . . . . . 6  set  j
32cv 1631 . . . . 5  class  j
4 ccld 16769 . . . . . 6  class  Clsd
53, 4cfv 5271 . . . . 5  class  ( Clsd `  j )
63, 5cin 3164 . . . 4  class  ( j  i^i  ( Clsd `  j
) )
7 c0 3468 . . . . 5  class  (/)
83cuni 3843 . . . . 5  class  U. j
97, 8cpr 3654 . . . 4  class  { (/) , 
U. j }
106, 9wceq 1632 . . 3  wff  ( j  i^i  ( Clsd `  j
) )  =  { (/)
,  U. j }
11 ctop 16647 . . 3  class  Top
1210, 2, 11crab 2560 . 2  class  { j  e.  Top  |  ( j  i^i  ( Clsd `  j ) )  =  { (/) ,  U. j } }
131, 12wceq 1632 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  17155
  Copyright terms: Public domain W3C validator