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