# Metamath Proof Explorer

## 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}×{A}\in \mathrm{Fin}$
2 1 ancoms ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to {B}×{A}\in \mathrm{Fin}$
3 pwfi ${⊢}{B}×{A}\in \mathrm{Fin}↔𝒫\left({B}×{A}\right)\in \mathrm{Fin}$
4 2 3 sylib ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to 𝒫\left({B}×{A}\right)\in \mathrm{Fin}$
5 mapsspw ${⊢}{{A}}^{{B}}\subseteq 𝒫\left({B}×{A}\right)$
6 ssfi ${⊢}\left(𝒫\left({B}×{A}\right)\in \mathrm{Fin}\wedge {{A}}^{{B}}\subseteq 𝒫\left({B}×{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}$