Theorem connsubclo

Description: If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015)

	Ref	Expression
Hypotheses	connsubclo.1	$$⊢X=\bigcup J$$
	connsubclo.3	$$⊢\phi \to A\subseteq X$$
	connsubclo.4	$$⊢\phi \to J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$
	connsubclo.5	$$⊢\phi \to B\in J$$
	connsubclo.6	$$⊢\phi \to B\cap A\ne \varnothing$$
	connsubclo.7	$$⊢\phi \to B\in \mathrm{Clsd}\left(J\right)$$
Assertion	connsubclo	$$⊢\phi \to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		connsubclo.1	$$⊢X=\bigcup J$$
2		connsubclo.3	$$⊢\phi \to A\subseteq X$$
3		connsubclo.4	$$⊢\phi \to J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$
4		connsubclo.5	$$⊢\phi \to B\in J$$
5		connsubclo.6	$$⊢\phi \to B\cap A\ne \varnothing$$
6		connsubclo.7	$$⊢\phi \to B\in \mathrm{Clsd}\left(J\right)$$
7		eqid	$$⊢\bigcup \left(J{\upharpoonright }_{𝑡}A\right)=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
8		cldrcl	$$⊢B\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
9	6 8	syl	$$⊢\phi \to J\in \mathrm{Top}$$
10	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
11	9 10	syl	$$⊢\phi \to X\in J$$
12	11 2	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
13		elrestr	$$⊢\left(J\in \mathrm{Top}\wedge A\in \mathrm{V}\wedge B\in J\right)\to B\cap A\in \left(J{\upharpoonright }_{𝑡}A\right)$$
14	9 12 4 13	syl3anc	$$⊢\phi \to B\cap A\in \left(J{\upharpoonright }_{𝑡}A\right)$$
15		eqid	$$⊢B\cap A=B\cap A$$
16		ineq1	$$⊢x=B\to x\cap A=B\cap A$$
17	16	rspceeqv	$$⊢\left(B\in \mathrm{Clsd}\left(J\right)\wedge B\cap A=B\cap A\right)\to \exists x\in \mathrm{Clsd}\left(J\right)B\cap A=x\cap A$$
18	6 15 17	sylancl	$$⊢\phi \to \exists x\in \mathrm{Clsd}\left(J\right)B\cap A=x\cap A$$
19	1	restcld	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to \left(B\cap A\in \mathrm{Clsd}\left(J{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in \mathrm{Clsd}\left(J\right)B\cap A=x\cap A\right)$$
20	9 2 19	syl2anc	$$⊢\phi \to \left(B\cap A\in \mathrm{Clsd}\left(J{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in \mathrm{Clsd}\left(J\right)B\cap A=x\cap A\right)$$
21	18 20	mpbird	$$⊢\phi \to B\cap A\in \mathrm{Clsd}\left(J{\upharpoonright }_{𝑡}A\right)$$
22	7 3 14 5 21	connclo	$$⊢\phi \to B\cap A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
23	1	restuni	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq X\right)\to A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
24	9 2 23	syl2anc	$$⊢\phi \to A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
25	22 24	eqtr4d	$$⊢\phi \to B\cap A=A$$
26		sseqin2	$$⊢A\subseteq B\leftrightarrow B\cap A=A$$
27	25 26	sylibr	$$⊢\phi \to A\subseteq B$$