# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}\subseteq {D}\to \bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{y}\in {B}}{D}$

### Proof

Step Hyp Ref Expression
1 ssiun ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}\subseteq {D}\to {C}\subseteq \bigcup _{{y}\in {B}}{D}$
2 1 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}\subseteq {D}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq \bigcup _{{y}\in {B}}{D}$
3 iunss ${⊢}\bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{y}\in {B}}{D}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq \bigcup _{{y}\in {B}}{D}$
4 2 3 sylibr ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{C}\subseteq {D}\to \bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{y}\in {B}}{D}$