disjiun

Description: A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by Mario Carneiro, 14-Nov-2016)

		Ref	Expression
	Assertion	disjiun	$⊢ (\underset{x \in A}{Disj} B \land (C \subseteq A \land D \subseteq A \land C \cap D = \emptyset)) \to ⋃_{x \in C} B \cap ⋃_{x \in D} B = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-disj	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \forall y \exists^{*} x \in A y \in B$
2		elin	$⊢ y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B) \leftrightarrow (y \in ⋃_{x \in C} B \land y \in ⋃_{x \in D} B)$
3		eliun	$⊢ y \in ⋃_{x \in C} B \leftrightarrow \exists x \in C y \in B$
4		eliun	$⊢ y \in ⋃_{x \in D} B \leftrightarrow \exists x \in D y \in B$
5	3 4	anbi12i	$⊢ (y \in ⋃_{x \in C} B \land y \in ⋃_{x \in D} B) \leftrightarrow (\exists x \in C y \in B \land \exists x \in D y \in B)$
6	2 5	bitri	$⊢ y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B) \leftrightarrow (\exists x \in C y \in B \land \exists x \in D y \in B)$
7		nfv	$⊢ Ⅎ z y \in B$
8	7	rmo2	$⊢ \exists^{*} x \in A y \in B \leftrightarrow \exists z \forall x \in A (y \in B \to x = z)$
9		an4	$⊢ ((C \subseteq A \land D \subseteq A) \land (\exists x \in C y \in B \land \exists x \in D y \in B)) \leftrightarrow ((C \subseteq A \land \exists x \in C y \in B) \land (D \subseteq A \land \exists x \in D y \in B))$
10		ssralv	$⊢ C \subseteq A \to (\forall x \in A (y \in B \to x = z) \to \forall x \in C (y \in B \to x = z))$
11	10	impcom	$⊢ (\forall x \in A (y \in B \to x = z) \land C \subseteq A) \to \forall x \in C (y \in B \to x = z)$
12		r19.29	$⊢ (\forall x \in C (y \in B \to x = z) \land \exists x \in C y \in B) \to \exists x \in C ((y \in B \to x = z) \land y \in B)$
13		id	$⊢ (y \in B \to x = z) \to (y \in B \to x = z)$
14	13	imp	$⊢ ((y \in B \to x = z) \land y \in B) \to x = z$
15	14	eleq1d	$⊢ ((y \in B \to x = z) \land y \in B) \to (x \in C \leftrightarrow z \in C)$
16	15	biimpcd	$⊢ x \in C \to (((y \in B \to x = z) \land y \in B) \to z \in C)$
17	16	rexlimiv	$⊢ \exists x \in C ((y \in B \to x = z) \land y \in B) \to z \in C$
18	12 17	syl	$⊢ (\forall x \in C (y \in B \to x = z) \land \exists x \in C y \in B) \to z \in C$
19	18	ex	$⊢ \forall x \in C (y \in B \to x = z) \to (\exists x \in C y \in B \to z \in C)$
20	11 19	syl	$⊢ (\forall x \in A (y \in B \to x = z) \land C \subseteq A) \to (\exists x \in C y \in B \to z \in C)$
21	20	expimpd	$⊢ \forall x \in A (y \in B \to x = z) \to ((C \subseteq A \land \exists x \in C y \in B) \to z \in C)$
22		ssralv	$⊢ D \subseteq A \to (\forall x \in A (y \in B \to x = z) \to \forall x \in D (y \in B \to x = z))$
23	22	impcom	$⊢ (\forall x \in A (y \in B \to x = z) \land D \subseteq A) \to \forall x \in D (y \in B \to x = z)$
24		r19.29	$⊢ (\forall x \in D (y \in B \to x = z) \land \exists x \in D y \in B) \to \exists x \in D ((y \in B \to x = z) \land y \in B)$
25	14	eleq1d	$⊢ ((y \in B \to x = z) \land y \in B) \to (x \in D \leftrightarrow z \in D)$
26	25	biimpcd	$⊢ x \in D \to (((y \in B \to x = z) \land y \in B) \to z \in D)$
27	26	rexlimiv	$⊢ \exists x \in D ((y \in B \to x = z) \land y \in B) \to z \in D$
28	24 27	syl	$⊢ (\forall x \in D (y \in B \to x = z) \land \exists x \in D y \in B) \to z \in D$
29	28	ex	$⊢ \forall x \in D (y \in B \to x = z) \to (\exists x \in D y \in B \to z \in D)$
30	23 29	syl	$⊢ (\forall x \in A (y \in B \to x = z) \land D \subseteq A) \to (\exists x \in D y \in B \to z \in D)$
31	30	expimpd	$⊢ \forall x \in A (y \in B \to x = z) \to ((D \subseteq A \land \exists x \in D y \in B) \to z \in D)$
32	21 31	anim12d	$⊢ \forall x \in A (y \in B \to x = z) \to (((C \subseteq A \land \exists x \in C y \in B) \land (D \subseteq A \land \exists x \in D y \in B)) \to (z \in C \land z \in D))$
33		inelcm	$⊢ (z \in C \land z \in D) \to C \cap D \neq \emptyset$
34	32 33	syl6	$⊢ \forall x \in A (y \in B \to x = z) \to (((C \subseteq A \land \exists x \in C y \in B) \land (D \subseteq A \land \exists x \in D y \in B)) \to C \cap D \neq \emptyset)$
35	34	exlimiv	$⊢ \exists z \forall x \in A (y \in B \to x = z) \to (((C \subseteq A \land \exists x \in C y \in B) \land (D \subseteq A \land \exists x \in D y \in B)) \to C \cap D \neq \emptyset)$
36	9 35	syl5bi	$⊢ \exists z \forall x \in A (y \in B \to x = z) \to (((C \subseteq A \land D \subseteq A) \land (\exists x \in C y \in B \land \exists x \in D y \in B)) \to C \cap D \neq \emptyset)$
37	36	expd	$⊢ \exists z \forall x \in A (y \in B \to x = z) \to ((C \subseteq A \land D \subseteq A) \to ((\exists x \in C y \in B \land \exists x \in D y \in B) \to C \cap D \neq \emptyset))$
38	8 37	sylbi	$⊢ \exists^{*} x \in A y \in B \to ((C \subseteq A \land D \subseteq A) \to ((\exists x \in C y \in B \land \exists x \in D y \in B) \to C \cap D \neq \emptyset))$
39	38	impcom	$⊢ ((C \subseteq A \land D \subseteq A) \land \exists^{*} x \in A y \in B) \to ((\exists x \in C y \in B \land \exists x \in D y \in B) \to C \cap D \neq \emptyset)$
40	6 39	syl5bi	$⊢ ((C \subseteq A \land D \subseteq A) \land \exists^{*} x \in A y \in B) \to (y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B) \to C \cap D \neq \emptyset)$
41	40	necon2bd	$⊢ ((C \subseteq A \land D \subseteq A) \land \exists^{*} x \in A y \in B) \to (C \cap D = \emptyset \to \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B))$
42	41	impancom	$⊢ ((C \subseteq A \land D \subseteq A) \land C \cap D = \emptyset) \to (\exists^{*} x \in A y \in B \to \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B))$
43	42	3impa	$⊢ (C \subseteq A \land D \subseteq A \land C \cap D = \emptyset) \to (\exists^{*} x \in A y \in B \to \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B))$
44	43	alimdv	$⊢ (C \subseteq A \land D \subseteq A \land C \cap D = \emptyset) \to (\forall y \exists^{*} x \in A y \in B \to \forall y \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B))$
45	1 44	syl5bi	$⊢ (C \subseteq A \land D \subseteq A \land C \cap D = \emptyset) \to (\underset{x \in A}{Disj} B \to \forall y \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B))$
46	45	impcom	$⊢ (\underset{x \in A}{Disj} B \land (C \subseteq A \land D \subseteq A \land C \cap D = \emptyset)) \to \forall y \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B)$
47		eq0	$⊢ ⋃_{x \in C} B \cap ⋃_{x \in D} B = \emptyset \leftrightarrow \forall y \neg y \in (⋃_{x \in C} B \cap ⋃_{x \in D} B)$
48	46 47	sylibr	$⊢ (\underset{x \in A}{Disj} B \land (C \subseteq A \land D \subseteq A \land C \cap D = \emptyset)) \to ⋃_{x \in C} B \cap ⋃_{x \in D} B = \emptyset$

Metamath Proof Explorer

Theorem disjiun

Proof