Metamath Proof Explorer


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 ( ( 𝐴𝑉 ∧ ∀ 𝑥𝐴 𝑥𝐵 ) → 𝐴 ≼ ( 𝐴 × 𝐵 ) )