Theorem mapfi

Description: Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011)

	Ref	Expression
Assertion	mapfi	|- ( ( A e. Fin /\ B e. Fin ) -> ( A ^m B ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		xpfi	|- ( ( B e. Fin /\ A e. Fin ) -> ( B X. A ) e. Fin )
2	1	ancoms	|- ( ( A e. Fin /\ B e. Fin ) -> ( B X. A ) e. Fin )
3		pwfi	|- ( ( B X. A ) e. Fin <-> ~P ( B X. A ) e. Fin )
4	2 3	sylib	|- ( ( A e. Fin /\ B e. Fin ) -> ~P ( B X. A ) e. Fin )
5		mapsspw	|- ( A ^m B ) C_ ~P ( B X. A )
6		ssfi	|- ( ( ~P ( B X. A ) e. Fin /\ ( A ^m B ) C_ ~P ( B X. A ) ) -> ( A ^m B ) e. Fin )
7	4 5 6	sylancl	|- ( ( A e. Fin /\ B e. Fin ) -> ( A ^m B ) e. Fin )