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 ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( 𝐴 ⊔ 𝐵 ) ≺ ω )

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