unconn

Description: The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 11-Jun-2014)

		Ref	Expression
	Assertion	unconn	$⊢ (J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land A \cap B \neq \emptyset) \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} (A \cup B) \in Conn)$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x x \in (A \cap B)$
2		uniiun	$⊢ ⋃ \{A, B\} = ⋃_{k \in \{A, B\}} k$
3		simpl1	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to J \in TopOn (X)$
4		toponmax	$⊢ J \in TopOn (X) \to X \in J$
5	3 4	syl	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to X \in J$
6		simpl2l	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to A \subseteq X$
7	5 6	ssexd	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to A \in V$
8		simpl2r	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to B \subseteq X$
9	5 8	ssexd	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to B \in V$
10		uniprg	$⊢ (A \in V \land B \in V) \to ⋃ \{A, B\} = A \cup B$
11	7 9 10	syl2anc	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to ⋃ \{A, B\} = A \cup B$
12	2 11	eqtr3id	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to ⋃_{k \in \{A, B\}} k = A \cup B$
13	12	oveq2d	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to J ↾_{𝑡} ⋃_{k \in \{A, B\}} k = J ↾_{𝑡} (A \cup B)$
14		vex	$⊢ k \in V$
15	14	elpr	$⊢ k \in \{A, B\} \leftrightarrow (k = A \lor k = B)$
16		simpl2	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to (A \subseteq X \land B \subseteq X)$
17		sseq1	$⊢ k = A \to (k \subseteq X \leftrightarrow A \subseteq X)$
18	17	biimprd	$⊢ k = A \to (A \subseteq X \to k \subseteq X)$
19		sseq1	$⊢ k = B \to (k \subseteq X \leftrightarrow B \subseteq X)$
20	19	biimprd	$⊢ k = B \to (B \subseteq X \to k \subseteq X)$
21	18 20	jaoa	$⊢ (k = A \lor k = B) \to ((A \subseteq X \land B \subseteq X) \to k \subseteq X)$
22	16 21	mpan9	$⊢ (((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \land (k = A \lor k = B)) \to k \subseteq X$
23	15 22	sylan2b	$⊢ (((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \land k \in \{A, B\}) \to k \subseteq X$
24		simpl3	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to x \in (A \cap B)$
25		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
26	24 25	sylib	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to (x \in A \land x \in B)$
27		eleq2	$⊢ k = A \to (x \in k \leftrightarrow x \in A)$
28	27	biimprd	$⊢ k = A \to (x \in A \to x \in k)$
29		eleq2	$⊢ k = B \to (x \in k \leftrightarrow x \in B)$
30	29	biimprd	$⊢ k = B \to (x \in B \to x \in k)$
31	28 30	jaoa	$⊢ (k = A \lor k = B) \to ((x \in A \land x \in B) \to x \in k)$
32	26 31	mpan9	$⊢ (((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \land (k = A \lor k = B)) \to x \in k$
33	15 32	sylan2b	$⊢ (((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \land k \in \{A, B\}) \to x \in k$
34		simpr	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)$
35		oveq2	$⊢ k = A \to J ↾_{𝑡} k = J ↾_{𝑡} A$
36	35	eleq1d	$⊢ k = A \to (J ↾_{𝑡} k \in Conn \leftrightarrow J ↾_{𝑡} A \in Conn)$
37	36	biimprd	$⊢ k = A \to (J ↾_{𝑡} A \in Conn \to J ↾_{𝑡} k \in Conn)$
38		oveq2	$⊢ k = B \to J ↾_{𝑡} k = J ↾_{𝑡} B$
39	38	eleq1d	$⊢ k = B \to (J ↾_{𝑡} k \in Conn \leftrightarrow J ↾_{𝑡} B \in Conn)$
40	39	biimprd	$⊢ k = B \to (J ↾_{𝑡} B \in Conn \to J ↾_{𝑡} k \in Conn)$
41	37 40	jaoa	$⊢ (k = A \lor k = B) \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} k \in Conn)$
42	34 41	mpan9	$⊢ (((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \land (k = A \lor k = B)) \to J ↾_{𝑡} k \in Conn$
43	15 42	sylan2b	$⊢ (((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \land k \in \{A, B\}) \to J ↾_{𝑡} k \in Conn$
44	3 23 33 43	iunconn	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to J ↾_{𝑡} ⋃_{k \in \{A, B\}} k \in Conn$
45	13 44	eqeltrrd	$⊢ ((J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \land (J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn)) \to J ↾_{𝑡} (A \cup B) \in Conn$
46	45	ex	$⊢ (J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land x \in (A \cap B)) \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} (A \cup B) \in Conn)$
47	46	3expia	$⊢ (J \in TopOn (X) \land (A \subseteq X \land B \subseteq X)) \to (x \in (A \cap B) \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} (A \cup B) \in Conn))$
48	47	exlimdv	$⊢ (J \in TopOn (X) \land (A \subseteq X \land B \subseteq X)) \to (\exists x x \in (A \cap B) \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} (A \cup B) \in Conn))$
49	1 48	syl5bi	$⊢ (J \in TopOn (X) \land (A \subseteq X \land B \subseteq X)) \to (A \cap B \neq \emptyset \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} (A \cup B) \in Conn))$
50	49	3impia	$⊢ (J \in TopOn (X) \land (A \subseteq X \land B \subseteq X) \land A \cap B \neq \emptyset) \to ((J ↾_{𝑡} A \in Conn \land J ↾_{𝑡} B \in Conn) \to J ↾_{𝑡} (A \cup B) \in Conn)$

Metamath Proof Explorer

Theorem unconn

Proof