This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isconn

Description: The predicate J is a connected topology . (Contributed by FL, 17-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 isconn.1 
 |-  X = U. J
2 id 
 |-  ( j = J -> j = J )
3 fveq2 
 |-  ( j = J -> ( Clsd ` j ) = ( Clsd ` J ) )
4 2 3 ineq12d 
 |-  ( j = J -> ( j i^i ( Clsd ` j ) ) = ( J i^i ( Clsd ` J ) ) )
5 unieq 
 |-  ( j = J -> U. j = U. J )
6 5 1 eqtr4di 
 |-  ( j = J -> U. j = X )
7 6 preq2d 
 |-  ( j = J -> { (/) , U. j } = { (/) , X } )
8 4 7 eqeq12d 
 |-  ( j = J -> ( ( j i^i ( Clsd ` j ) ) = { (/) , U. j } <-> ( J i^i ( Clsd ` J ) ) = { (/) , X } ) )
9 df-conn 
 |-  Conn = { j e. Top | ( j i^i ( Clsd ` j ) ) = { (/) , U. j } }
10 8 9 elrab2 
 |-  ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) )