connsuba

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

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		resttopon	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \in TopOn (A)$
2		dfconn2	$⊢ J ↾_{𝑡} A \in TopOn (A) \to (J ↾_{𝑡} A \in Conn \leftrightarrow \forall u \in (J ↾_{𝑡} A) \forall v \in (J ↾_{𝑡} A) ((u \neq \emptyset \land v \neq \emptyset \land u \cap v = \emptyset) \to u \cup v \neq A))$
3	1 2	syl	$⊢ (J \in TopOn (X) \land A \subseteq X) \to (J ↾_{𝑡} A \in Conn \leftrightarrow \forall u \in (J ↾_{𝑡} A) \forall v \in (J ↾_{𝑡} A) ((u \neq \emptyset \land v \neq \emptyset \land u \cap v = \emptyset) \to u \cup v \neq A))$
4		vex	$⊢ x \in V$
5	4	inex1	$⊢ x \cap A \in V$
6	5	a1i	$⊢ ((J \in TopOn (X) \land A \subseteq X) \land x \in J) \to x \cap A \in V$
7		toponmax	$⊢ J \in TopOn (X) \to X \in J$
8	7	adantr	$⊢ (J \in TopOn (X) \land A \subseteq X) \to X \in J$
9		simpr	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \subseteq X$
10	8 9	ssexd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \in V$
11		elrest	$⊢ (J \in TopOn (X) \land A \in V) \to (u \in (J ↾_{𝑡} A) \leftrightarrow \exists x \in J u = x \cap A)$
12	10 11	syldan	$⊢ (J \in TopOn (X) \land A \subseteq X) \to (u \in (J ↾_{𝑡} A) \leftrightarrow \exists x \in J u = x \cap A)$
13		vex	$⊢ y \in V$
14	13	inex1	$⊢ y \cap A \in V$
15	14	a1i	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land y \in J) \to y \cap A \in V$
16		elrest	$⊢ (J \in TopOn (X) \land A \in V) \to (v \in (J ↾_{𝑡} A) \leftrightarrow \exists y \in J v = y \cap A)$
17	10 16	syldan	$⊢ (J \in TopOn (X) \land A \subseteq X) \to (v \in (J ↾_{𝑡} A) \leftrightarrow \exists y \in J v = y \cap A)$
18	17	adantr	$⊢ ((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \to (v \in (J ↾_{𝑡} A) \leftrightarrow \exists y \in J v = y \cap A)$
19		simplr	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to u = x \cap A$
20	19	neeq1d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to (u \neq \emptyset \leftrightarrow x \cap A \neq \emptyset)$
21		simpr	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to v = y \cap A$
22	21	neeq1d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to (v \neq \emptyset \leftrightarrow y \cap A \neq \emptyset)$
23	19 21	ineq12d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to u \cap v = (x \cap A) \cap (y \cap A)$
24		inindir	$⊢ (x \cap y) \cap A = (x \cap A) \cap (y \cap A)$
25	23 24	eqtr4di	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to u \cap v = (x \cap y) \cap A$
26	25	eqeq1d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to (u \cap v = \emptyset \leftrightarrow (x \cap y) \cap A = \emptyset)$
27	20 22 26	3anbi123d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to ((u \neq \emptyset \land v \neq \emptyset \land u \cap v = \emptyset) \leftrightarrow (x \cap A \neq \emptyset \land y \cap A \neq \emptyset \land (x \cap y) \cap A = \emptyset))$
28	19 21	uneq12d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to u \cup v = (x \cap A) \cup (y \cap A)$
29		indir	$⊢ (x \cup y) \cap A = (x \cap A) \cup (y \cap A)$
30	28 29	eqtr4di	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to u \cup v = (x \cup y) \cap A$
31	30	neeq1d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to (u \cup v \neq A \leftrightarrow (x \cup y) \cap A \neq A)$
32	27 31	imbi12d	$⊢ (((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \land v = y \cap A) \to (((u \neq \emptyset \land v \neq \emptyset \land u \cap v = \emptyset) \to u \cup v \neq A) \leftrightarrow ((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))$
33	15 18 32	ralxfr2d	$⊢ ((J \in TopOn (X) \land A \subseteq X) \land u = x \cap A) \to (\forall v \in (J ↾_{𝑡} A) ((u \neq \emptyset \land v \neq \emptyset \land u \cap v = \emptyset) \to u \cup v \neq A) \leftrightarrow \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))$
34	6 12 33	ralxfr2d	$⊢ (J \in TopOn (X) \land A \subseteq X) \to (\forall u \in (J ↾_{𝑡} A) \forall v \in (J ↾_{𝑡} A) ((u \neq \emptyset \land v \neq \emptyset \land u \cap v = \emptyset) \to u \cup v \neq A) \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))$
35	3 34	bitrd	$⊢ (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))$

Metamath Proof Explorer

Theorem connsuba

Proof