Theorem unifi

Description: The finite union of finite sets is finite. Exercise 13 of Enderton p. 144. (Contributed by NM, 22-Aug-2008) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	unifi	|- ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		dfss3	|- ( A C_ Fin <-> A. x e. A x e. Fin )
2		uniiun	|- U. A = U_ x e. A x
3		iunfi	|- ( ( A e. Fin /\ A. x e. A x e. Fin ) -> U_ x e. A x e. Fin )
4	2 3	eqeltrid	|- ( ( A e. Fin /\ A. x e. A x e. Fin ) -> U. A e. Fin )
5	1 4	sylan2b	|- ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin )