Theorem iunss2

Description: A subclass condition on the members of two indexed classes C ( x ) and D ( y ) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of TakeutiZaring p. 59. Compare uniss2 . (Contributed by NM, 9-Dec-2004)

	Ref	Expression
Assertion	iunss2	$$⊢\forall x\in A\exists y\in BC\subseteq D\to \bigcup _{x\in A}C\subseteq \bigcup _{y\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		ssiun	$$⊢\exists y\in BC\subseteq D\to C\subseteq \bigcup _{y\in B}D$$
2	1	ralimi	$$⊢\forall x\in A\exists y\in BC\subseteq D\to \forall x\in AC\subseteq \bigcup _{y\in B}D$$
3		iunss	$$⊢\bigcup _{x\in A}C\subseteq \bigcup _{y\in B}D\leftrightarrow \forall x\in AC\subseteq \bigcup _{y\in B}D$$
4	2 3	sylibr	$$⊢\forall x\in A\exists y\in BC\subseteq D\to \bigcup _{x\in A}C\subseteq \bigcup _{y\in B}D$$