This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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