Theorem disjiun2

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

	Ref	Expression
Hypotheses	disjiun2.1	$$⊢\phi \to \underset{x\in A}{Disj}B$$
	disjiun2.2	$$⊢\phi \to C\subseteq A$$
	disjiun2.3	$$⊢\phi \to D\in \left(A\setminus C\right)$$
	disjiun2.4	$$⊢x=D\to B=E$$
Assertion	disjiun2	$$⊢\phi \to \bigcup _{x\in C}B\cap E=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disjiun2.1	$$⊢\phi \to \underset{x\in A}{Disj}B$$
2		disjiun2.2	$$⊢\phi \to C\subseteq A$$
3		disjiun2.3	$$⊢\phi \to D\in \left(A\setminus C\right)$$
4		disjiun2.4	$$⊢x=D\to B=E$$
5	4	iunxsng	$$⊢D\in \left(A\setminus C\right)\to \bigcup _{x\in \left\{D\right\}}B=E$$
6	3 5	syl	$$⊢\phi \to \bigcup _{x\in \left\{D\right\}}B=E$$
7	6	ineq2d	$$⊢\phi \to \bigcup _{x\in C}B\cap \bigcup _{x\in \left\{D\right\}}B=\bigcup _{x\in C}B\cap E$$
8		eldifi	$$⊢D\in \left(A\setminus C\right)\to D\in A$$
9		snssi	$$⊢D\in A\to \left\{D\right\}\subseteq A$$
10	3 8 9	3syl	$$⊢\phi \to \left\{D\right\}\subseteq A$$
11	3	eldifbd	$$⊢\phi \to \neg D\in C$$
12		disjsn	$$⊢C\cap \left\{D\right\}=\varnothing \leftrightarrow \neg D\in C$$
13	11 12	sylibr	$$⊢\phi \to C\cap \left\{D\right\}=\varnothing$$
14		disjiun	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(C\subseteq A\wedge \left\{D\right\}\subseteq A\wedge C\cap \left\{D\right\}=\varnothing \right)\right)\to \bigcup _{x\in C}B\cap \bigcup _{x\in \left\{D\right\}}B=\varnothing$$
15	1 2 10 13 14	syl13anc	$$⊢\phi \to \bigcup _{x\in C}B\cap \bigcup _{x\in \left\{D\right\}}B=\varnothing$$
16	7 15	eqtr3d	$$⊢\phi \to \bigcup _{x\in C}B\cap E=\varnothing$$