Theorem mptfi

Description: A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	mptfi	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		funfn	⊢ ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3	1 2	mpbi	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	4	dmmptss	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴
6		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ Fin )
7	5 6	mpan2	⊢ ( 𝐴 ∈ Fin → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ Fin )
8		fnfi	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ Fin ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ Fin )
9	3 7 8	sylancr	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ Fin )