Theorem unfi2

Description: The union of two finite sets is finite. Part of Corollary 6K of Enderton p. 144. This version of unfi is useful only if we assume the Axiom of Infinity (see comments in fin2inf ). (Contributed by NM, 22-Oct-2004) (Revised by Mario Carneiro, 27-Apr-2015)

	Ref	Expression
Assertion	unfi2	|- ( ( A ~< _om /\ B ~< _om ) -> ( A u. B ) ~< _om )

Proof

Step	Hyp	Ref	Expression
1		isfinite2	|- ( A ~< _om -> A e. Fin )
2		isfinite2	|- ( B ~< _om -> B e. Fin )
3		unfi	|- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
4	1 2 3	syl2an	|- ( ( A ~< _om /\ B ~< _om ) -> ( A u. B ) e. Fin )
5		fin2inf	|- ( A ~< _om -> _om e. _V )
6	5	adantr	|- ( ( A ~< _om /\ B ~< _om ) -> _om e. _V )
7		isfiniteg	|- ( _om e. _V -> ( ( A u. B ) e. Fin <-> ( A u. B ) ~< _om ) )
8	6 7	syl	|- ( ( A ~< _om /\ B ~< _om ) -> ( ( A u. B ) e. Fin <-> ( A u. B ) ~< _om ) )
9	4 8	mpbid	|- ( ( A ~< _om /\ B ~< _om ) -> ( A u. B ) ~< _om )