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 = J
Assertion isconn J Conn J Top J Clsd J = X

Proof

Step Hyp Ref Expression
1 isconn.1 X = J
2 id j = J j = J
3 fveq2 j = J Clsd j = Clsd J
4 2 3 ineq12d j = J j Clsd j = J Clsd J
5 unieq j = J j = J
6 5 1 eqtr4di j = J j = X
7 6 preq2d j = J j = X
8 4 7 eqeq12d j = J j Clsd j = j J Clsd J = X
9 df-conn Conn = j Top | j Clsd j = j
10 8 9 elrab2 J Conn J Top J Clsd J = X