Metamath Proof Explorer

Theorem unctb

Description: The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006) (Proof shortened by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion unctb ⊢ A ≼ ω ∧ B ≼ ω → A ∪ B ≼ ω

Proof

Step Hyp Ref Expression
1 ctex ⊢ A ≼ ω → A ∈ V
2 ctex ⊢ B ≼ ω → B ∈ V
3 undjudom ⊢ A ∈ V ∧ B ∈ V → A ∪ B ≼ A ⊔︀ B
4 1 2 3 syl2an ⊢ A ≼ ω ∧ B ≼ ω → A ∪ B ≼ A ⊔︀ B
5 djudom1 ⊢ A ≼ ω ∧ B ∈ V → A ⊔︀ B ≼ ω ⊔︀ B
6 2 5 sylan2 ⊢ A ≼ ω ∧ B ≼ ω → A ⊔︀ B ≼ ω ⊔︀ B
7 simpr ⊢ A ≼ ω ∧ B ≼ ω → B ≼ ω
8 omex ⊢ ω ∈ V
9 djudom2 ⊢ B ≼ ω ∧ ω ∈ V → ω ⊔︀ B ≼ ω ⊔︀ ω
10 7 8 9 sylancl ⊢ A ≼ ω ∧ B ≼ ω → ω ⊔︀ B ≼ ω ⊔︀ ω
11 domtr ⊢ A ⊔︀ B ≼ ω ⊔︀ B ∧ ω ⊔︀ B ≼ ω ⊔︀ ω → A ⊔︀ B ≼ ω ⊔︀ ω
12 6 10 11 syl2anc ⊢ A ≼ ω ∧ B ≼ ω → A ⊔︀ B ≼ ω ⊔︀ ω
13 8 8 xpex ⊢ ω × ω ∈ V
14 xp2dju ⊢ 2 𝑜 × ω = ω ⊔︀ ω
15 ordom ⊢ Ord ⁡ ω
16 2onn ⊢ 2 𝑜 ∈ ω
17 ordelss ⊢ Ord ⁡ ω ∧ 2 𝑜 ∈ ω → 2 𝑜 ⊆ ω
18 15 16 17 mp2an ⊢ 2 𝑜 ⊆ ω
19 xpss1 ⊢ 2 𝑜 ⊆ ω → 2 𝑜 × ω ⊆ ω × ω
20 18 19 ax-mp ⊢ 2 𝑜 × ω ⊆ ω × ω
21 14 20 eqsstrri ⊢ ω ⊔︀ ω ⊆ ω × ω
22 ssdomg ⊢ ω × ω ∈ V → ω ⊔︀ ω ⊆ ω × ω → ω ⊔︀ ω ≼ ω × ω
23 13 21 22 mp2 ⊢ ω ⊔︀ ω ≼ ω × ω
24 xpomen ⊢ ω × ω ≈ ω
25 domentr ⊢ ω ⊔︀ ω ≼ ω × ω ∧ ω × ω ≈ ω → ω ⊔︀ ω ≼ ω
26 23 24 25 mp2an ⊢ ω ⊔︀ ω ≼ ω
27 domtr ⊢ A ⊔︀ B ≼ ω ⊔︀ ω ∧ ω ⊔︀ ω ≼ ω → A ⊔︀ B ≼ ω
28 12 26 27 sylancl ⊢ A ≼ ω ∧ B ≼ ω → A ⊔︀ B ≼ ω
29 domtr ⊢ A ∪ B ≼ A ⊔︀ B ∧ A ⊔︀ B ≼ ω → A ∪ B ≼ ω
30 4 28 29 syl2anc ⊢ A ≼ ω ∧ B ≼ ω → A ∪ B ≼ ω