Theorem conndisj

Description: If a topology is connected, its underlying set can't be partitioned into two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008) (Proof shortened 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$$
	conndisj.4	$$⊢\phi \to B\in J$$
	conndisj.5	$$⊢\phi \to B\ne \varnothing$$
	conndisj.6	$$⊢\phi \to A\cap B=\varnothing$$
Assertion	conndisj	$$⊢\phi \to A\cup B\ne 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		conndisj.4	$$⊢\phi \to B\in J$$
6		conndisj.5	$$⊢\phi \to B\ne \varnothing$$
7		conndisj.6	$$⊢\phi \to A\cap B=\varnothing$$
8		elssuni	$$⊢A\in J\to A\subseteq \bigcup J$$
9	3 8	syl	$$⊢\phi \to A\subseteq \bigcup J$$
10	9 1	sseqtrrdi	$$⊢\phi \to A\subseteq X$$
11		uneqdifeq	$$⊢\left(A\subseteq X\wedge A\cap B=\varnothing \right)\to \left(A\cup B=X\leftrightarrow X\setminus A=B\right)$$
12	10 7 11	syl2anc	$$⊢\phi \to \left(A\cup B=X\leftrightarrow X\setminus A=B\right)$$
13		simpr	$$⊢\left(\phi \wedge X\setminus A=B\right)\to X\setminus A=B$$
14	13	difeq2d	$$⊢\left(\phi \wedge X\setminus A=B\right)\to X\setminus \left(X\setminus A\right)=X\setminus B$$
15		dfss4	$$⊢A\subseteq X\leftrightarrow X\setminus \left(X\setminus A\right)=A$$
16	10 15	sylib	$$⊢\phi \to X\setminus \left(X\setminus A\right)=A$$
17	16	adantr	$$⊢\left(\phi \wedge X\setminus A=B\right)\to X\setminus \left(X\setminus A\right)=A$$
18	2	adantr	$$⊢\left(\phi \wedge X\setminus A=B\right)\to J\in \mathrm{Conn}$$
19	5	adantr	$$⊢\left(\phi \wedge X\setminus A=B\right)\to B\in J$$
20	6	adantr	$$⊢\left(\phi \wedge X\setminus A=B\right)\to B\ne \varnothing$$
21	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)$$
22	21	simplbi	$$⊢J\in \mathrm{Conn}\to J\in \mathrm{Top}$$
23	2 22	syl	$$⊢\phi \to J\in \mathrm{Top}$$
24	1	opncld	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to X\setminus A\in \mathrm{Clsd}\left(J\right)$$
25	23 3 24	syl2anc	$$⊢\phi \to X\setminus A\in \mathrm{Clsd}\left(J\right)$$
26	25	adantr	$$⊢\left(\phi \wedge X\setminus A=B\right)\to X\setminus A\in \mathrm{Clsd}\left(J\right)$$
27	13 26	eqeltrrd	$$⊢\left(\phi \wedge X\setminus A=B\right)\to B\in \mathrm{Clsd}\left(J\right)$$
28	1 18 19 20 27	connclo	$$⊢\left(\phi \wedge X\setminus A=B\right)\to B=X$$
29	28	difeq2d	$$⊢\left(\phi \wedge X\setminus A=B\right)\to X\setminus B=X\setminus X$$
30		difid	$$⊢X\setminus X=\varnothing$$
31	29 30	eqtrdi	$$⊢\left(\phi \wedge X\setminus A=B\right)\to X\setminus B=\varnothing$$
32	14 17 31	3eqtr3d	$$⊢\left(\phi \wedge X\setminus A=B\right)\to A=\varnothing$$
33	32	ex	$$⊢\phi \to \left(X\setminus A=B\to A=\varnothing \right)$$
34	12 33	sylbid	$$⊢\phi \to \left(A\cup B=X\to A=\varnothing \right)$$
35	34	necon3d	$$⊢\phi \to \left(A\ne \varnothing \to A\cup B\ne X\right)$$
36	4 35	mpd	$$⊢\phi \to A\cup B\ne X$$