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 \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) = \{\emptyset, X\})$

Step	Hyp	Ref	Expression
1		isconn.1	$⊢ X = ⋃ J$
2		id	$⊢ j = J \to j = J$
3		fveq2	$⊢ j = J \to Clsd (j) = Clsd (J)$
4	2 3	ineq12d	$⊢ j = J \to j \cap Clsd (j) = J \cap Clsd (J)$
5		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
6	5 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
7	6	preq2d	$⊢ j = J \to \{\emptyset, ⋃ j\} = \{\emptyset, X\}$
8	4 7	eqeq12d	$⊢ j = J \to (j \cap Clsd (j) = \{\emptyset, ⋃ j\} \leftrightarrow J \cap Clsd (J) = \{\emptyset, X\})$
9		df-conn	$⊢ Conn = \{j \in Top \| j \cap Clsd (j) = \{\emptyset, ⋃ j\}\}$
10	8 9	elrab2	$⊢ J \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) = \{\emptyset, X\})$

Metamath Proof Explorer