djudisj

Description: Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014)

		Ref	Expression
	Assertion	djudisj	$⊢ A \cap B = \emptyset \to ⋃_{x \in A} (\{x\} \times C) \cap ⋃_{y \in B} (\{y\} \times D) = \emptyset$

Step	Hyp	Ref	Expression
1		djussxp	$⊢ ⋃_{x \in A} (\{x\} \times C) \subseteq A \times V$
2		incom	$⊢ (A \times V) \cap ⋃_{y \in B} (\{y\} \times D) = ⋃_{y \in B} (\{y\} \times D) \cap (A \times V)$
3		djussxp	$⊢ ⋃_{y \in B} (\{y\} \times D) \subseteq B \times V$
4		incom	$⊢ (B \times V) \cap (A \times V) = (A \times V) \cap (B \times V)$
5		xpdisj1	$⊢ A \cap B = \emptyset \to (A \times V) \cap (B \times V) = \emptyset$
6	4 5	eqtrid	$⊢ A \cap B = \emptyset \to (B \times V) \cap (A \times V) = \emptyset$
7		ssdisj	$⊢ (⋃_{y \in B} (\{y\} \times D) \subseteq B \times V \land (B \times V) \cap (A \times V) = \emptyset) \to ⋃_{y \in B} (\{y\} \times D) \cap (A \times V) = \emptyset$
8	3 6 7	sylancr	$⊢ A \cap B = \emptyset \to ⋃_{y \in B} (\{y\} \times D) \cap (A \times V) = \emptyset$
9	2 8	eqtrid	$⊢ A \cap B = \emptyset \to (A \times V) \cap ⋃_{y \in B} (\{y\} \times D) = \emptyset$
10		ssdisj	$⊢ (⋃_{x \in A} (\{x\} \times C) \subseteq A \times V \land (A \times V) \cap ⋃_{y \in B} (\{y\} \times D) = \emptyset) \to ⋃_{x \in A} (\{x\} \times C) \cap ⋃_{y \in B} (\{y\} \times D) = \emptyset$
11	1 9 10	sylancr	$⊢ A \cap B = \emptyset \to ⋃_{x \in A} (\{x\} \times C) \cap ⋃_{y \in B} (\{y\} \times D) = \emptyset$

Metamath Proof Explorer