Theorem uniss2

Description: A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of TakeutiZaring p. 59. See iunss2 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004)

	Ref	Expression
Assertion	uniss2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssuni	⊢ ( ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ⊆ ∪ 𝐵 )
2	1	expcom	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑥 ⊆ 𝑦 → 𝑥 ⊆ ∪ 𝐵 ) )
3	2	rexlimiv	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → 𝑥 ⊆ ∪ 𝐵 )
4	3	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ 𝐵 )
5		unissb	⊢ ( ∪ 𝐴 ⊆ ∪ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ 𝐵 )
6	4 5	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵 )