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

Metamath Proof Explorer

Theorem djufi

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

Ref Expression
Assertion djufi ⊢ A ≺ ω ∧ B ≺ ω → A ⊔︀ B ≺ ω

Proof

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