Theorem disjiunel

Description: A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		disjiunel.1	$$⊢\phi \to \underset{x\in A}{Disj}B$$
2		disjiunel.2	$$⊢x=Y\to B=D$$
3		disjiunel.3	$$⊢\phi \to E\subseteq A$$
4		disjiunel.4	$$⊢\phi \to Y\in \left(A\setminus E\right)$$
5	4	eldifad	$$⊢\phi \to Y\in A$$
6	5	snssd	$$⊢\phi \to \left\{Y\right\}\subseteq A$$
7	3 6	unssd	$$⊢\phi \to E\cup \left\{Y\right\}\subseteq A$$
8		disjss1	$$⊢E\cup \left\{Y\right\}\subseteq A\to \left(\underset{x\in A}{Disj}B\to \underset{x\in E\cup \left\{Y\right\}}{Disj}B\right)$$
9	7 1 8	sylc	$$⊢\phi \to \underset{x\in E\cup \left\{Y\right\}}{Disj}B$$
10	4	eldifbd	$$⊢\phi \to \neg Y\in E$$
11	2	disjunsn	$$⊢\left(Y\in A\wedge \neg Y\in E\right)\to \left(\underset{x\in E\cup \left\{Y\right\}}{Disj}B\leftrightarrow \left(\underset{x\in E}{Disj}B\wedge \bigcup _{x\in E}B\cap D=\varnothing \right)\right)$$
12	5 10 11	syl2anc	$$⊢\phi \to \left(\underset{x\in E\cup \left\{Y\right\}}{Disj}B\leftrightarrow \left(\underset{x\in E}{Disj}B\wedge \bigcup _{x\in E}B\cap D=\varnothing \right)\right)$$
13	9 12	mpbid	$$⊢\phi \to \left(\underset{x\in E}{Disj}B\wedge \bigcup _{x\in E}B\cap D=\varnothing \right)$$
14	13	simprd	$$⊢\phi \to \bigcup _{x\in E}B\cap D=\varnothing$$