djufi

Description: The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004)

		Ref	Expression
	Assertion	djufi	$⊢ (A ≺ ω \land B ≺ ω) \to (A ⊔︀ B) ≺ ω$

Step	Hyp	Ref	Expression
1		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
2		0elon	$⊢ \emptyset \in On$
3		relsdom	$⊢ Rel ≺$
4	3	brrelex1i	$⊢ A ≺ ω \to A \in V$
5		xpsnen2g	$⊢ (\emptyset \in On \land A \in V) \to (\{\emptyset\} \times A) \approx A$
6	2 4 5	sylancr	$⊢ A ≺ ω \to (\{\emptyset\} \times A) \approx A$
7		sdomen1	$⊢ (\{\emptyset\} \times A) \approx A \to ((\{\emptyset\} \times A) ≺ ω \leftrightarrow A ≺ ω)$
8	6 7	syl	$⊢ A ≺ ω \to ((\{\emptyset\} \times A) ≺ ω \leftrightarrow A ≺ ω)$
9	8	ibir	$⊢ A ≺ ω \to (\{\emptyset\} \times A) ≺ ω$
10		1on	$⊢ 1_{𝑜} \in On$
11	3	brrelex1i	$⊢ B ≺ ω \to B \in V$
12		xpsnen2g	$⊢ (1_{𝑜} \in On \land B \in V) \to (\{1_{𝑜}\} \times B) \approx B$
13	10 11 12	sylancr	$⊢ B ≺ ω \to (\{1_{𝑜}\} \times B) \approx B$
14		sdomen1	$⊢ (\{1_{𝑜}\} \times B) \approx B \to ((\{1_{𝑜}\} \times B) ≺ ω \leftrightarrow B ≺ ω)$
15	13 14	syl	$⊢ B ≺ ω \to ((\{1_{𝑜}\} \times B) ≺ ω \leftrightarrow B ≺ ω)$
16	15	ibir	$⊢ B ≺ ω \to (\{1_{𝑜}\} \times B) ≺ ω$
17		unfi2	$⊢ ((\{\emptyset\} \times A) ≺ ω \land (\{1_{𝑜}\} \times B) ≺ ω) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) ≺ ω$
18	9 16 17	syl2an	$⊢ (A ≺ ω \land B ≺ ω) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) ≺ ω$
19	1 18	eqbrtrid	$⊢ (A ≺ ω \land B ≺ ω) \to (A ⊔︀ B) ≺ ω$

Metamath Proof Explorer