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

Metamath Proof Explorer

Theorem conntop

Description: A connected topology is a topology. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 14-Dec-2013)

		Ref	Expression
	Assertion	conntop	$⊢ J \in Conn \to J \in Top$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	isconn	$⊢ J \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) = \{\emptyset, ⋃ J\})$
3	2	simplbi	$⊢ J \in Conn \to J \in Top$