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 ~< _om /\ B ~< _om ) -> ( A |_| B ) ~< _om )

Proof

Step Hyp Ref Expression
1 df-dju 
 |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
2 0elon 
 |-  (/) e. On
3 relsdom 
 |-  Rel ~<
4 3 brrelex1i 
 |-  ( A ~< _om -> A e. _V )
5 xpsnen2g 
 |-  ( ( (/) e. On /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
6 2 4 5 sylancr 
 |-  ( A ~< _om -> ( { (/) } X. A ) ~~ A )
7 sdomen1 
 |-  ( ( { (/) } X. A ) ~~ A -> ( ( { (/) } X. A ) ~< _om <-> A ~< _om ) )
8 6 7 syl 
 |-  ( A ~< _om -> ( ( { (/) } X. A ) ~< _om <-> A ~< _om ) )
9 8 ibir 
 |-  ( A ~< _om -> ( { (/) } X. A ) ~< _om )
10 1on 
 |-  1o e. On
11 3 brrelex1i 
 |-  ( B ~< _om -> B e. _V )
12 xpsnen2g 
 |-  ( ( 1o e. On /\ B e. _V ) -> ( { 1o } X. B ) ~~ B )
13 10 11 12 sylancr 
 |-  ( B ~< _om -> ( { 1o } X. B ) ~~ B )
14 sdomen1 
 |-  ( ( { 1o } X. B ) ~~ B -> ( ( { 1o } X. B ) ~< _om <-> B ~< _om ) )
15 13 14 syl 
 |-  ( B ~< _om -> ( ( { 1o } X. B ) ~< _om <-> B ~< _om ) )
16 15 ibir 
 |-  ( B ~< _om -> ( { 1o } X. B ) ~< _om )
17 unfi2 
 |-  ( ( ( { (/) } X. A ) ~< _om /\ ( { 1o } X. B ) ~< _om ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~< _om )
18 9 16 17 syl2an 
 |-  ( ( A ~< _om /\ B ~< _om ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~< _om )
19 1 18 eqbrtrid 
 |-  ( ( A ~< _om /\ B ~< _om ) -> ( A |_| B ) ~< _om )