Metamath Proof Explorer

Theorem isconn2

Description: The predicate J is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypothesis isconn.1 
|- X = U. J
Assertion isconn2 
|- ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) )

Proof

Step Hyp Ref Expression
1 isconn.1 
 |-  X = U. J
2 1 isconn 
 |-  ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) )
3 eqss 
 |-  ( ( J i^i ( Clsd ` J ) ) = { (/) , X } <-> ( ( J i^i ( Clsd ` J ) ) C_ { (/) , X } /\ { (/) , X } C_ ( J i^i ( Clsd ` J ) ) ) )
4 0opn 
 |-  ( J e. Top -> (/) e. J )
5 0cld 
 |-  ( J e. Top -> (/) e. ( Clsd ` J ) )
6 4 5 elind 
 |-  ( J e. Top -> (/) e. ( J i^i ( Clsd ` J ) ) )
7 1 topopn 
 |-  ( J e. Top -> X e. J )
8 1 topcld 
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
9 7 8 elind 
 |-  ( J e. Top -> X e. ( J i^i ( Clsd ` J ) ) )
10 6 9 prssd 
 |-  ( J e. Top -> { (/) , X } C_ ( J i^i ( Clsd ` J ) ) )
11 10 biantrud 
 |-  ( J e. Top -> ( ( J i^i ( Clsd ` J ) ) C_ { (/) , X } <-> ( ( J i^i ( Clsd ` J ) ) C_ { (/) , X } /\ { (/) , X } C_ ( J i^i ( Clsd ` J ) ) ) ) )
12 3 11 bitr4id 
 |-  ( J e. Top -> ( ( J i^i ( Clsd ` J ) ) = { (/) , X } <-> ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) )
13 12 pm5.32i 
 |-  ( ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) )
14 2 13 bitri 
 |-  ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) )