Theorem 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	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ω ) → ∪ 𝐴 ≼ ω )