Theorem connclo

Description: The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015)

	Ref	Expression
Hypotheses	isconn.1	$$⊢X=\bigcup J$$
	connclo.1	$$⊢\phi \to J\in \mathrm{Conn}$$
	connclo.2	$$⊢\phi \to A\in J$$
	connclo.3	$$⊢\phi \to A\ne \varnothing$$
	connclo.4	$$⊢\phi \to A\in \mathrm{Clsd}\left(J\right)$$
Assertion	connclo	$$⊢\phi \to A=X$$

Proof

Step	Hyp	Ref	Expression
1		isconn.1	$$⊢X=\bigcup J$$
2		connclo.1	$$⊢\phi \to J\in \mathrm{Conn}$$
3		connclo.2	$$⊢\phi \to A\in J$$
4		connclo.3	$$⊢\phi \to A\ne \varnothing$$
5		connclo.4	$$⊢\phi \to A\in \mathrm{Clsd}\left(J\right)$$
6	4	neneqd	$$⊢\phi \to \neg A=\varnothing$$
7	3 5	elind	$$⊢\phi \to A\in \left(J\cap \mathrm{Clsd}\left(J\right)\right)$$
8	1	isconn	$$⊢J\in \mathrm{Conn}\leftrightarrow \left(J\in \mathrm{Top}\wedge J\cap \mathrm{Clsd}\left(J\right)=\left\{\varnothing ,X\right\}\right)$$
9	8	simprbi	$$⊢J\in \mathrm{Conn}\to J\cap \mathrm{Clsd}\left(J\right)=\left\{\varnothing ,X\right\}$$
10	2 9	syl	$$⊢\phi \to J\cap \mathrm{Clsd}\left(J\right)=\left\{\varnothing ,X\right\}$$
11	7 10	eleqtrd	$$⊢\phi \to A\in \left\{\varnothing ,X\right\}$$
12		elpri	$$⊢A\in \left\{\varnothing ,X\right\}\to \left(A=\varnothing \vee A=X\right)$$
13	11 12	syl	$$⊢\phi \to \left(A=\varnothing \vee A=X\right)$$
14	13	ord	$$⊢\phi \to \left(\neg A=\varnothing \to A=X\right)$$
15	6 14	mpd	$$⊢\phi \to A=X$$