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 ≼ ω \land B ≼ ω) \to (A \cup B) ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		ctex	$⊢ A ≼ ω \to A \in V$
2		ctex	$⊢ B ≼ ω \to B \in V$
3		undjudom	$⊢ (A \in V \land B \in V) \to (A \cup B) ≼ (A ⊔︀ B)$
4	1 2 3	syl2an	$⊢ (A ≼ ω \land B ≼ ω) \to (A \cup B) ≼ (A ⊔︀ B)$
5		djudom1	$⊢ (A ≼ ω \land B \in V) \to (A ⊔︀ B) ≼ (ω ⊔︀ B)$
6	2 5	sylan2	$⊢ (A ≼ ω \land B ≼ ω) \to (A ⊔︀ B) ≼ (ω ⊔︀ B)$
7		simpr	$⊢ (A ≼ ω \land B ≼ ω) \to B ≼ ω$
8		omex	$⊢ ω \in V$
9		djudom2	$⊢ (B ≼ ω \land ω \in V) \to (ω ⊔︀ B) ≼ (ω ⊔︀ ω)$
10	7 8 9	sylancl	$⊢ (A ≼ ω \land B ≼ ω) \to (ω ⊔︀ B) ≼ (ω ⊔︀ ω)$
11		domtr	$⊢ ((A ⊔︀ B) ≼ (ω ⊔︀ B) \land (ω ⊔︀ B) ≼ (ω ⊔︀ ω)) \to (A ⊔︀ B) ≼ (ω ⊔︀ ω)$
12	6 10 11	syl2anc	$⊢ (A ≼ ω \land B ≼ ω) \to (A ⊔︀ B) ≼ (ω ⊔︀ ω)$
13	8 8	xpex	$⊢ ω \times ω \in V$
14		xp2dju	$⊢ 2_{𝑜} \times ω = (ω ⊔︀ ω)$
15		ordom	$⊢ Ord ω$
16		2onn	$⊢ 2_{𝑜} \in ω$
17		ordelss	$⊢ (Ord ω \land 2_{𝑜} \in ω) \to 2_{𝑜} \subseteq ω$
18	15 16 17	mp2an	$⊢ 2_{𝑜} \subseteq ω$
19		xpss1	$⊢ 2_{𝑜} \subseteq ω \to 2_{𝑜} \times ω \subseteq ω \times ω$
20	18 19	ax-mp	$⊢ 2_{𝑜} \times ω \subseteq ω \times ω$
21	14 20	eqsstrri	$⊢ (ω ⊔︀ ω) \subseteq ω \times ω$
22		ssdomg	$⊢ ω \times ω \in V \to ((ω ⊔︀ ω) \subseteq ω \times ω \to (ω ⊔︀ ω) ≼ (ω \times ω))$
23	13 21 22	mp2	$⊢ (ω ⊔︀ ω) ≼ (ω \times ω)$
24		xpomen	$⊢ (ω \times ω) \approx ω$
25		domentr	$⊢ ((ω ⊔︀ ω) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (ω ⊔︀ ω) ≼ ω$
26	23 24 25	mp2an	$⊢ (ω ⊔︀ ω) ≼ ω$
27		domtr	$⊢ ((A ⊔︀ B) ≼ (ω ⊔︀ ω) \land (ω ⊔︀ ω) ≼ ω) \to (A ⊔︀ B) ≼ ω$
28	12 26 27	sylancl	$⊢ (A ≼ ω \land B ≼ ω) \to (A ⊔︀ B) ≼ ω$
29		domtr	$⊢ ((A \cup B) ≼ (A ⊔︀ B) \land (A ⊔︀ B) ≼ ω) \to (A \cup B) ≼ ω$
30	4 28 29	syl2anc	$⊢ (A ≼ ω \land B ≼ ω) \to (A \cup B) ≼ ω$

Metamath Proof Explorer

Theorem unctb

Proof