This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY ZFC Set Theory - add the Axiom of Choice AC equivalents: well-ordering, Zorn's lemma 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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ 𝐵 ) → ∪ 𝐴 ≼ ( 𝐴 × 𝐵 ) )