Theorem inunissunidif

Description: Theorem about subsets of the difference of unions. (Contributed by ML, 29-Mar-2021)

	Ref	Expression
Assertion	inunissunidif	$$⊢A\cap \bigcup C=\varnothing \to \left(A\subseteq \bigcup B\leftrightarrow A\subseteq \bigcup \left(B\setminus C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		reldisj	$$⊢A\subseteq \bigcup B\to \left(A\cap \bigcup C=\varnothing \leftrightarrow A\subseteq \bigcup B\setminus \bigcup C\right)$$
2		difunieq	$$⊢\bigcup B\setminus \bigcup C\subseteq \bigcup \left(B\setminus C\right)$$
3		sstr	$$⊢\left(A\subseteq \bigcup B\setminus \bigcup C\wedge \bigcup B\setminus \bigcup C\subseteq \bigcup \left(B\setminus C\right)\right)\to A\subseteq \bigcup \left(B\setminus C\right)$$
4	2 3	mpan2	$$⊢A\subseteq \bigcup B\setminus \bigcup C\to A\subseteq \bigcup \left(B\setminus C\right)$$
5	1 4	biimtrdi	$$⊢A\subseteq \bigcup B\to \left(A\cap \bigcup C=\varnothing \to A\subseteq \bigcup \left(B\setminus C\right)\right)$$
6	5	com12	$$⊢A\cap \bigcup C=\varnothing \to \left(A\subseteq \bigcup B\to A\subseteq \bigcup \left(B\setminus C\right)\right)$$
7		difss	$$⊢B\setminus C\subseteq B$$
8	7	unissi	$$⊢\bigcup \left(B\setminus C\right)\subseteq \bigcup B$$
9		sstr	$$⊢\left(A\subseteq \bigcup \left(B\setminus C\right)\wedge \bigcup \left(B\setminus C\right)\subseteq \bigcup B\right)\to A\subseteq \bigcup B$$
10	8 9	mpan2	$$⊢A\subseteq \bigcup \left(B\setminus C\right)\to A\subseteq \bigcup B$$
11	6 10	impbid1	$$⊢A\cap \bigcup C=\varnothing \to \left(A\subseteq \bigcup B\leftrightarrow A\subseteq \bigcup \left(B\setminus C\right)\right)$$