Theorem djufi

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

	Ref	Expression
Assertion	djufi	⊢ ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( 𝐴 ⊔ 𝐵 ) ≺ ω )

Proof

Step	Hyp	Ref	Expression
1		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
2		0elon	⊢ ∅ ∈ On
3		relsdom	⊢ Rel ≺
4	3	brrelex1i	⊢ ( 𝐴 ≺ ω → 𝐴 ∈ V )
5		xpsnen2g	⊢ ( ( ∅ ∈ On ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
6	2 4 5	sylancr	⊢ ( 𝐴 ≺ ω → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
7		sdomen1	⊢ ( ( { ∅ } × 𝐴 ) ≈ 𝐴 → ( ( { ∅ } × 𝐴 ) ≺ ω ↔ 𝐴 ≺ ω ) )
8	6 7	syl	⊢ ( 𝐴 ≺ ω → ( ( { ∅ } × 𝐴 ) ≺ ω ↔ 𝐴 ≺ ω ) )
9	8	ibir	⊢ ( 𝐴 ≺ ω → ( { ∅ } × 𝐴 ) ≺ ω )
10		1on	⊢ 1o ∈ On
11	3	brrelex1i	⊢ ( 𝐵 ≺ ω → 𝐵 ∈ V )
12		xpsnen2g	⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ V ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
13	10 11 12	sylancr	⊢ ( 𝐵 ≺ ω → ( { 1o } × 𝐵 ) ≈ 𝐵 )
14		sdomen1	⊢ ( ( { 1o } × 𝐵 ) ≈ 𝐵 → ( ( { 1o } × 𝐵 ) ≺ ω ↔ 𝐵 ≺ ω ) )
15	13 14	syl	⊢ ( 𝐵 ≺ ω → ( ( { 1o } × 𝐵 ) ≺ ω ↔ 𝐵 ≺ ω ) )
16	15	ibir	⊢ ( 𝐵 ≺ ω → ( { 1o } × 𝐵 ) ≺ ω )
17		unfi2	⊢ ( ( ( { ∅ } × 𝐴 ) ≺ ω ∧ ( { 1o } × 𝐵 ) ≺ ω ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≺ ω )
18	9 16 17	syl2an	⊢ ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≺ ω )
19	1 18	eqbrtrid	⊢ ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( 𝐴 ⊔ 𝐵 ) ≺ ω )