Theorem unifi2

Description: The finite union of finite sets is finite. Exercise 13 of Enderton p. 144. This version of unifi is useful only if we assume the Axiom of Infinity (see comments in fin2inf ). (Contributed by NM, 11-Mar-2006)

	Ref	Expression
Assertion	unifi2	|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> U. A ~< _om )

Proof

Step	Hyp	Ref	Expression
1		isfinite2	|- ( A ~< _om -> A e. Fin )
2		isfinite2	|- ( x ~< _om -> x e. Fin )
3	2	ralimi	|- ( A. x e. A x ~< _om -> A. x e. A x e. Fin )
4		dfss3	|- ( A C_ Fin <-> A. x e. A x e. Fin )
5	3 4	sylibr	|- ( A. x e. A x ~< _om -> A C_ Fin )
6		unifi	|- ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin )
7	1 5 6	syl2an	|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> U. A e. Fin )
8		fin2inf	|- ( A ~< _om -> _om e. _V )
9	8	adantr	|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> _om e. _V )
10		isfiniteg	|- ( _om e. _V -> ( U. A e. Fin <-> U. A ~< _om ) )
11	9 10	syl	|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> ( U. A e. Fin <-> U. A ~< _om ) )
12	7 11	mpbid	|- ( ( A ~< _om /\ A. x e. A x ~< _om ) -> U. A ~< _om )