mapfi

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

		Ref	Expression
	Assertion	mapfi	$⊢ (A \in Fin \land B \in Fin) \to A^{B} \in Fin$

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

Metamath Proof Explorer