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 )