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 Cardinal number arithmetic using Axiom of Choice unictb
Description: The countable union of countable sets is countable. Theorem 6Q of
Enderton p. 159. See iunctb for indexed union version.
(Contributed by NM , 26-Mar-2006)
Ref
Expression
Assertion
unictb ⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ω ) → ∪ 𝐴 ≼ ω )
Proof
Step
Hyp
Ref
Expression
1
uniiun ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
2
iunctb ⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 𝑥 ≼ ω )
3
1 2
eqbrtrid ⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ω ) → ∪ 𝐴 ≼ ω )