Theorem disjss2

Description: If each element of a collection is contained in a disjoint collection, the original collection is also disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	disjss2	$$⊢\forall x\in AB\subseteq C\to \left(\underset{x\in A}{Disj}C\to \underset{x\in A}{Disj}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢B\subseteq C\to \left(y\in B\to y\in C\right)$$
2	1	ralimi	$$⊢\forall x\in AB\subseteq C\to \forall x\in A\left(y\in B\to y\in C\right)$$
3		rmoim	$$⊢\forall x\in A\left(y\in B\to y\in C\right)\to \left({\exists }^{*}x\in Ay\in C\to {\exists }^{*}x\in Ay\in B\right)$$
4	2 3	syl	$$⊢\forall x\in AB\subseteq C\to \left({\exists }^{*}x\in Ay\in C\to {\exists }^{*}x\in Ay\in B\right)$$
5	4	alimdv	$$⊢\forall x\in AB\subseteq C\to \left(\forall y{\exists }^{*}x\in Ay\in C\to \forall y{\exists }^{*}x\in Ay\in B\right)$$
6		df-disj	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \forall y{\exists }^{*}x\in Ay\in C$$
7		df-disj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\in Ay\in B$$
8	5 6 7	3imtr4g	$$⊢\forall x\in AB\subseteq C\to \left(\underset{x\in A}{Disj}C\to \underset{x\in A}{Disj}B\right)$$