Theorem mapfi

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

	Ref	Expression
Assertion	mapfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ↑m 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		xpfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝐵 × 𝐴 ) ∈ Fin )
2	1	ancoms	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐵 × 𝐴 ) ∈ Fin )
3		pwfi	⊢ ( ( 𝐵 × 𝐴 ) ∈ Fin ↔ 𝒫 ( 𝐵 × 𝐴 ) ∈ Fin )
4	2 3	sylib	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → 𝒫 ( 𝐵 × 𝐴 ) ∈ Fin )
5		mapsspw	⊢ ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 )
6		ssfi	⊢ ( ( 𝒫 ( 𝐵 × 𝐴 ) ∈ Fin ∧ ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 ) ) → ( 𝐴 ↑m 𝐵 ) ∈ Fin )
7	4 5 6	sylancl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ↑m 𝐵 ) ∈ Fin )