Theorem nconnsubb

Description: Disconnectedness for a subspace. (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 10-Mar-2015)

	Ref	Expression
Hypotheses	nconnsubb.2	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	nconnsubb.3	$$⊢\phi \to A\subseteq X$$
	nconnsubb.4	$$⊢\phi \to U\in J$$
	nconnsubb.5	$$⊢\phi \to V\in J$$
	nconnsubb.6	$$⊢\phi \to U\cap A\ne \varnothing$$
	nconnsubb.7	$$⊢\phi \to V\cap A\ne \varnothing$$
	nconnsubb.8	$$⊢\phi \to \left(U\cap V\right)\cap A=\varnothing$$
	nconnsubb.9	$$⊢\phi \to A\subseteq U\cup V$$
Assertion	nconnsubb	$$⊢\phi \to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$

Proof

Step	Hyp	Ref	Expression
1		nconnsubb.2	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
2		nconnsubb.3	$$⊢\phi \to A\subseteq X$$
3		nconnsubb.4	$$⊢\phi \to U\in J$$
4		nconnsubb.5	$$⊢\phi \to V\in J$$
5		nconnsubb.6	$$⊢\phi \to U\cap A\ne \varnothing$$
6		nconnsubb.7	$$⊢\phi \to V\cap A\ne \varnothing$$
7		nconnsubb.8	$$⊢\phi \to \left(U\cap V\right)\cap A=\varnothing$$
8		nconnsubb.9	$$⊢\phi \to A\subseteq U\cup V$$
9		connsuba	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge A\subseteq X\right)\to \left(J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}\leftrightarrow \forall x\in J\forall y\in J\left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\to \left(x\cup y\right)\cap A\ne A\right)\right)$$
10	1 2 9	syl2anc	$$⊢\phi \to \left(J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}\leftrightarrow \forall x\in J\forall y\in J\left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\to \left(x\cup y\right)\cap A\ne A\right)\right)$$
11	5 6 7	3jca	$$⊢\phi \to \left(U\cap A\ne \varnothing \wedge V\cap A\ne \varnothing \wedge \left(U\cap V\right)\cap A=\varnothing \right)$$
12		ineq1	$$⊢x=U\to x\cap A=U\cap A$$
13	12	neeq1d	$$⊢x=U\to \left(x\cap A\ne \varnothing \leftrightarrow U\cap A\ne \varnothing \right)$$
14		ineq1	$$⊢x=U\to x\cap y=U\cap y$$
15	14	ineq1d	$$⊢x=U\to \left(x\cap y\right)\cap A=\left(U\cap y\right)\cap A$$
16	15	eqeq1d	$$⊢x=U\to \left(\left(x\cap y\right)\cap A=\varnothing \leftrightarrow \left(U\cap y\right)\cap A=\varnothing \right)$$
17	13 16	3anbi13d	$$⊢x=U\to \left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\leftrightarrow \left(U\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(U\cap y\right)\cap A=\varnothing \right)\right)$$
18		uneq1	$$⊢x=U\to x\cup y=U\cup y$$
19	18	ineq1d	$$⊢x=U\to \left(x\cup y\right)\cap A=\left(U\cup y\right)\cap A$$
20	19	neeq1d	$$⊢x=U\to \left(\left(x\cup y\right)\cap A\ne A\leftrightarrow \left(U\cup y\right)\cap A\ne A\right)$$
21	17 20	imbi12d	$$⊢x=U\to \left(\left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\to \left(x\cup y\right)\cap A\ne A\right)\leftrightarrow \left(\left(U\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(U\cap y\right)\cap A=\varnothing \right)\to \left(U\cup y\right)\cap A\ne A\right)\right)$$
22		ineq1	$$⊢y=V\to y\cap A=V\cap A$$
23	22	neeq1d	$$⊢y=V\to \left(y\cap A\ne \varnothing \leftrightarrow V\cap A\ne \varnothing \right)$$
24		ineq2	$$⊢y=V\to U\cap y=U\cap V$$
25	24	ineq1d	$$⊢y=V\to \left(U\cap y\right)\cap A=\left(U\cap V\right)\cap A$$
26	25	eqeq1d	$$⊢y=V\to \left(\left(U\cap y\right)\cap A=\varnothing \leftrightarrow \left(U\cap V\right)\cap A=\varnothing \right)$$
27	23 26	3anbi23d	$$⊢y=V\to \left(\left(U\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(U\cap y\right)\cap A=\varnothing \right)\leftrightarrow \left(U\cap A\ne \varnothing \wedge V\cap A\ne \varnothing \wedge \left(U\cap V\right)\cap A=\varnothing \right)\right)$$
28		sseqin2	$$⊢A\subseteq U\cup y\leftrightarrow \left(U\cup y\right)\cap A=A$$
29	28	necon3bbii	$$⊢\neg A\subseteq U\cup y\leftrightarrow \left(U\cup y\right)\cap A\ne A$$
30		uneq2	$$⊢y=V\to U\cup y=U\cup V$$
31	30	sseq2d	$$⊢y=V\to \left(A\subseteq U\cup y\leftrightarrow A\subseteq U\cup V\right)$$
32	31	notbid	$$⊢y=V\to \left(\neg A\subseteq U\cup y\leftrightarrow \neg A\subseteq U\cup V\right)$$
33	29 32	bitr3id	$$⊢y=V\to \left(\left(U\cup y\right)\cap A\ne A\leftrightarrow \neg A\subseteq U\cup V\right)$$
34	27 33	imbi12d	$$⊢y=V\to \left(\left(\left(U\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(U\cap y\right)\cap A=\varnothing \right)\to \left(U\cup y\right)\cap A\ne A\right)\leftrightarrow \left(\left(U\cap A\ne \varnothing \wedge V\cap A\ne \varnothing \wedge \left(U\cap V\right)\cap A=\varnothing \right)\to \neg A\subseteq U\cup V\right)\right)$$
35	21 34	rspc2v	$$⊢\left(U\in J\wedge V\in J\right)\to \left(\forall x\in J\forall y\in J\left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\to \left(x\cup y\right)\cap A\ne A\right)\to \left(\left(U\cap A\ne \varnothing \wedge V\cap A\ne \varnothing \wedge \left(U\cap V\right)\cap A=\varnothing \right)\to \neg A\subseteq U\cup V\right)\right)$$
36	3 4 35	syl2anc	$$⊢\phi \to \left(\forall x\in J\forall y\in J\left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\to \left(x\cup y\right)\cap A\ne A\right)\to \left(\left(U\cap A\ne \varnothing \wedge V\cap A\ne \varnothing \wedge \left(U\cap V\right)\cap A=\varnothing \right)\to \neg A\subseteq U\cup V\right)\right)$$
37	11 36	mpid	$$⊢\phi \to \left(\forall x\in J\forall y\in J\left(\left(x\cap A\ne \varnothing \wedge y\cap A\ne \varnothing \wedge \left(x\cap y\right)\cap A=\varnothing \right)\to \left(x\cup y\right)\cap A\ne A\right)\to \neg A\subseteq U\cup V\right)$$
38	10 37	sylbid	$$⊢\phi \to \left(J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}\to \neg A\subseteq U\cup V\right)$$
39	8 38	mt2d	$$⊢\phi \to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$