iunconn

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014)

	Ref	Expression
Hypotheses	iunconn.2	$⊢ φ \to J \in TopOn (X)$
	iunconn.3	$⊢ (φ \land k \in A) \to B \subseteq X$
	iunconn.4	$⊢ (φ \land k \in A) \to P \in B$
	iunconn.5	$⊢ (φ \land k \in A) \to J ↾_{𝑡} B \in Conn$
Assertion	iunconn	$⊢ φ \to J ↾_{𝑡} ⋃_{k \in A} B \in Conn$

Proof

Step	Hyp	Ref	Expression
1		iunconn.2	$⊢ φ \to J \in TopOn (X)$
2		iunconn.3	$⊢ (φ \land k \in A) \to B \subseteq X$
3		iunconn.4	$⊢ (φ \land k \in A) \to P \in B$
4		iunconn.5	$⊢ (φ \land k \in A) \to J ↾_{𝑡} B \in Conn$
5		simpr	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to ⋃_{k \in A} B \subseteq u \cup v$
6		simplr1	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to u \cap ⋃_{k \in A} B \neq \emptyset$
7		n0	$⊢ u \cap ⋃_{k \in A} B \neq \emptyset \leftrightarrow \exists v v \in (u \cap ⋃_{k \in A} B)$
8		elinel2	$⊢ v \in (u \cap ⋃_{k \in A} B) \to v \in ⋃_{k \in A} B$
9		eliun	$⊢ v \in ⋃_{k \in A} B \leftrightarrow \exists k \in A v \in B$
10		rexn0	$⊢ \exists k \in A v \in B \to A \neq \emptyset$
11	9 10	sylbi	$⊢ v \in ⋃_{k \in A} B \to A \neq \emptyset$
12	8 11	syl	$⊢ v \in (u \cap ⋃_{k \in A} B) \to A \neq \emptyset$
13	12	exlimiv	$⊢ \exists v v \in (u \cap ⋃_{k \in A} B) \to A \neq \emptyset$
14	7 13	sylbi	$⊢ u \cap ⋃_{k \in A} B \neq \emptyset \to A \neq \emptyset$
15	6 14	syl	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to A \neq \emptyset$
16		simplll	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to φ$
17	3	ralrimiva	$⊢ φ \to \forall k \in A P \in B$
18	16 17	syl	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to \forall k \in A P \in B$
19		r19.2z	$⊢ (A \neq \emptyset \land \forall k \in A P \in B) \to \exists k \in A P \in B$
20	15 18 19	syl2anc	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to \exists k \in A P \in B$
21		eliun	$⊢ P \in ⋃_{k \in A} B \leftrightarrow \exists k \in A P \in B$
22	20 21	sylibr	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to P \in ⋃_{k \in A} B$
23	5 22	sseldd	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to P \in (u \cup v)$
24		elun	$⊢ P \in (u \cup v) \leftrightarrow (P \in u \lor P \in v)$
25	23 24	sylib	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to (P \in u \lor P \in v)$
26	16 1	syl	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to J \in TopOn (X)$
27	16 2	sylan	$⊢ ((((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \land k \in A) \to B \subseteq X$
28	16 3	sylan	$⊢ ((((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \land k \in A) \to P \in B$
29	16 4	sylan	$⊢ ((((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \land k \in A) \to J ↾_{𝑡} B \in Conn$
30		simpllr	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to (u \in J \land v \in J)$
31	30	simpld	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to u \in J$
32	30	simprd	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to v \in J$
33		simplr2	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to v \cap ⋃_{k \in A} B \neq \emptyset$
34		simplr3	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to u \cap v \subseteq X ∖ ⋃_{k \in A} B$
35		nfv	$⊢ Ⅎ k (φ \land (u \in J \land v \in J))$
36		nfcv	$⊢ \underline{Ⅎ} k u$
37		nfiu1	$⊢ \underline{Ⅎ} k ⋃_{k \in A} B$
38	36 37	nfin	$⊢ \underline{Ⅎ} k (u \cap ⋃_{k \in A} B)$
39		nfcv	$⊢ \underline{Ⅎ} k \emptyset$
40	38 39	nfne	$⊢ Ⅎ k u \cap ⋃_{k \in A} B \neq \emptyset$
41		nfcv	$⊢ \underline{Ⅎ} k v$
42	41 37	nfin	$⊢ \underline{Ⅎ} k (v \cap ⋃_{k \in A} B)$
43	42 39	nfne	$⊢ Ⅎ k v \cap ⋃_{k \in A} B \neq \emptyset$
44		nfcv	$⊢ \underline{Ⅎ} k (u \cap v)$
45		nfcv	$⊢ \underline{Ⅎ} k X$
46	45 37	nfdif	$⊢ \underline{Ⅎ} k (X ∖ ⋃_{k \in A} B)$
47	44 46	nfss	$⊢ Ⅎ k u \cap v \subseteq X ∖ ⋃_{k \in A} B$
48	40 43 47	nf3an	$⊢ Ⅎ k (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)$
49	35 48	nfan	$⊢ Ⅎ k ((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B))$
50	36 41	nfun	$⊢ \underline{Ⅎ} k (u \cup v)$
51	37 50	nfss	$⊢ Ⅎ k ⋃_{k \in A} B \subseteq u \cup v$
52	49 51	nfan	$⊢ Ⅎ k (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v)$
53	26 27 28 29 31 32 33 34 5 52	iunconnlem	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to \neg P \in u$
54		incom	$⊢ v \cap u = u \cap v$
55	54 34	eqsstrid	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to v \cap u \subseteq X ∖ ⋃_{k \in A} B$
56		uncom	$⊢ u \cup v = v \cup u$
57	5 56	sseqtrdi	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to ⋃_{k \in A} B \subseteq v \cup u$
58	26 27 28 29 32 31 6 55 57 52	iunconnlem	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to \neg P \in v$
59		ioran	$⊢ \neg (P \in u \lor P \in v) \leftrightarrow (\neg P \in u \land \neg P \in v)$
60	53 58 59	sylanbrc	$⊢ (((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \land ⋃_{k \in A} B \subseteq u \cup v) \to \neg (P \in u \lor P \in v)$
61	25 60	pm2.65da	$⊢ ((φ \land (u \in J \land v \in J)) \land (u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B)) \to \neg ⋃_{k \in A} B \subseteq u \cup v$
62	61	ex	$⊢ (φ \land (u \in J \land v \in J)) \to ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v)$
63	62	ralrimivva	$⊢ φ \to \forall u \in J \forall v \in J ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v)$
64	2	ralrimiva	$⊢ φ \to \forall k \in A B \subseteq X$
65		iunss	$⊢ ⋃_{k \in A} B \subseteq X \leftrightarrow \forall k \in A B \subseteq X$
66	64 65	sylibr	$⊢ φ \to ⋃_{k \in A} B \subseteq X$
67		connsub	$⊢ (J \in TopOn (X) \land ⋃_{k \in A} B \subseteq X) \to (J ↾_{𝑡} ⋃_{k \in A} B \in Conn \leftrightarrow \forall u \in J \forall v \in J ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v))$
68	1 66 67	syl2anc	$⊢ φ \to (J ↾_{𝑡} ⋃_{k \in A} B \in Conn \leftrightarrow \forall u \in J \forall v \in J ((u \cap ⋃_{k \in A} B \neq \emptyset \land v \cap ⋃_{k \in A} B \neq \emptyset \land u \cap v \subseteq X ∖ ⋃_{k \in A} B) \to \neg ⋃_{k \in A} B \subseteq u \cup v))$
69	63 68	mpbird	$⊢ φ \to J ↾_{𝑡} ⋃_{k \in A} B \in Conn$

Metamath Proof Explorer

Theorem iunconn

Proof