Theorem unidom

Description: An upper bound for the cardinality of a union. Theorem 10.47 of TakeutiZaring p. 98. (Contributed by NM, 25-Mar-2006) (Proof shortened by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Assertion	unidom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ 𝐵 ) → ∪ 𝐴 ≼ ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
2		iundom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝑥 ≼ ( 𝐴 × 𝐵 ) )
3	1 2	eqbrtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ 𝐵 ) → ∪ 𝐴 ≼ ( 𝐴 × 𝐵 ) )