isconn2

Description: The predicate J is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Hypothesis	isconn.1	$⊢ X = ⋃ J$
	Assertion	isconn2	$⊢ J \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) \subseteq \{\emptyset, X\})$

Step	Hyp	Ref	Expression
1		isconn.1	$⊢ X = ⋃ J$
2	1	isconn	$⊢ J \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) = \{\emptyset, X\})$
3		eqss	$⊢ J \cap Clsd (J) = \{\emptyset, X\} \leftrightarrow (J \cap Clsd (J) \subseteq \{\emptyset, X\} \land \{\emptyset, X\} \subseteq J \cap Clsd (J))$
4		0opn	$⊢ J \in Top \to \emptyset \in J$
5		0cld	$⊢ J \in Top \to \emptyset \in Clsd (J)$
6	4 5	elind	$⊢ J \in Top \to \emptyset \in (J \cap Clsd (J))$
7	1	topopn	$⊢ J \in Top \to X \in J$
8	1	topcld	$⊢ J \in Top \to X \in Clsd (J)$
9	7 8	elind	$⊢ J \in Top \to X \in (J \cap Clsd (J))$
10	6 9	prssd	$⊢ J \in Top \to \{\emptyset, X\} \subseteq J \cap Clsd (J)$
11	10	biantrud	$⊢ J \in Top \to (J \cap Clsd (J) \subseteq \{\emptyset, X\} \leftrightarrow (J \cap Clsd (J) \subseteq \{\emptyset, X\} \land \{\emptyset, X\} \subseteq J \cap Clsd (J)))$
12	3 11	bitr4id	$⊢ J \in Top \to (J \cap Clsd (J) = \{\emptyset, X\} \leftrightarrow J \cap Clsd (J) \subseteq \{\emptyset, X\})$
13	12	pm5.32i	$⊢ (J \in Top \land J \cap Clsd (J) = \{\emptyset, X\}) \leftrightarrow (J \in Top \land J \cap Clsd (J) \subseteq \{\emptyset, X\})$
14	2 13	bitri	$⊢ J \in Conn \leftrightarrow (J \in Top \land J \cap Clsd (J) \subseteq \{\emptyset, X\})$

Metamath Proof Explorer