indisconn

Description: The indiscrete topology (or trivial topology) on any set is connected. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Assertion	indisconn	$⊢ \{\emptyset, A\} \in Conn$

Proof

Step	Hyp	Ref	Expression
1		indistop	$⊢ \{\emptyset, A\} \in Top$
2		inss1	$⊢ \{\emptyset, A\} \cap Clsd (\{\emptyset, A\}) \subseteq \{\emptyset, A\}$
3		indislem	$⊢ \{\emptyset, I (A)\} = \{\emptyset, A\}$
4	2 3	sseqtrri	$⊢ \{\emptyset, A\} \cap Clsd (\{\emptyset, A\}) \subseteq \{\emptyset, I (A)\}$
5		indisuni	$⊢ I (A) = ⋃ \{\emptyset, A\}$
6	5	isconn2	$⊢ \{\emptyset, A\} \in Conn \leftrightarrow (\{\emptyset, A\} \in Top \land \{\emptyset, A\} \cap Clsd (\{\emptyset, A\}) \subseteq \{\emptyset, I (A)\})$
7	1 4 6	mpbir2an	$⊢ \{\emptyset, A\} \in Conn$

Metamath Proof Explorer

Theorem indisconn

Proof