Theorem 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	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Conn}$$

Proof

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