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 ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴𝐵 ) ≼ ω )

Proof

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