disjiun2

Description: In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Step	Hyp	Ref	Expression
1		disjiun2.1	$⊢ φ \to \underset{x \in A}{Disj} B$
2		disjiun2.2	$⊢ φ \to C \subseteq A$
3		disjiun2.3	$⊢ φ \to D \in (A ∖ C)$
4		disjiun2.4	$⊢ x = D \to B = E$
5	4	iunxsng	$⊢ D \in (A ∖ C) \to ⋃_{x \in \{D\}} B = E$
6	3 5	syl	$⊢ φ \to ⋃_{x \in \{D\}} B = E$
7	6	ineq2d	$⊢ φ \to ⋃_{x \in C} B \cap ⋃_{x \in \{D\}} B = ⋃_{x \in C} B \cap E$
8		eldifi	$⊢ D \in (A ∖ C) \to D \in A$
9		snssi	$⊢ D \in A \to \{D\} \subseteq A$
10	3 8 9	3syl	$⊢ φ \to \{D\} \subseteq A$
11	3	eldifbd	$⊢ φ \to \neg D \in C$
12		disjsn	$⊢ C \cap \{D\} = \emptyset \leftrightarrow \neg D \in C$
13	11 12	sylibr	$⊢ φ \to C \cap \{D\} = \emptyset$
14		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$
15	1 2 10 13 14	syl13anc	$⊢ φ \to ⋃_{x \in C} B \cap ⋃_{x \in \{D\}} B = \emptyset$
16	7 15	eqtr3d	$⊢ φ \to ⋃_{x \in C} B \cap E = \emptyset$

Metamath Proof Explorer