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 } ) )