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