This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∀ x ∈ A ∃ y ∈ B C ⊆ D → ⋃ x ∈ A C ⊆ ⋃ y ∈ B D

Proof

Step Hyp Ref Expression
1 ssiun ⊢ ∃ y ∈ B C ⊆ D → C ⊆ ⋃ y ∈ B D
2 1 ralimi ⊢ ∀ x ∈ A ∃ y ∈ B C ⊆ D → ∀ x ∈ A C ⊆ ⋃ y ∈ B D
3 iunss ⊢ ⋃ x ∈ A C ⊆ ⋃ y ∈ B D ↔ ∀ x ∈ A C ⊆ ⋃ y ∈ B D
4 2 3 sylibr ⊢ ∀ x ∈ A ∃ y ∈ B C ⊆ D → ⋃ x ∈ A C ⊆ ⋃ y ∈ B D