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	$⊢ φ \to J \in TopOn (X)$
	nconnsubb.3	$⊢ φ \to A \subseteq X$
	nconnsubb.4	$⊢ φ \to U \in J$
	nconnsubb.5	$⊢ φ \to V \in J$
	nconnsubb.6	$⊢ φ \to U \cap A \neq \emptyset$
	nconnsubb.7	$⊢ φ \to V \cap A \neq \emptyset$
	nconnsubb.8	$⊢ φ \to (U \cap V) \cap A = \emptyset$
	nconnsubb.9	$⊢ φ \to A \subseteq U \cup V$
Assertion	nconnsubb	$⊢ φ \to \neg J ↾_{𝑡} A \in Conn$

Proof

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

Metamath Proof Explorer

Theorem nconnsubb

Proof