Theorem mapfi

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

	Ref	Expression
Assertion	mapfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A^B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		xpfi	$$⊢\left(B\in \mathrm{Fin}\wedge A\in \mathrm{Fin}\right)\to B\times A\in \mathrm{Fin}$$
2	1	ancoms	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to B\times A\in \mathrm{Fin}$$
3		pwfi	$$⊢B\times A\in \mathrm{Fin}\leftrightarrow 𝒫\left(B\times A\right)\in \mathrm{Fin}$$
4	2 3	sylib	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to 𝒫\left(B\times A\right)\in \mathrm{Fin}$$
5		mapsspw	$$⊢A^B\subseteq 𝒫\left(B\times A\right)$$
6		ssfi	$$⊢\left(𝒫\left(B\times A\right)\in \mathrm{Fin}\wedge A^B\subseteq 𝒫\left(B\times A\right)\right)\to A^B\in \mathrm{Fin}$$
7	4 5 6	sylancl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A^B\in \mathrm{Fin}$$