Theorem mptfi

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

	Ref	Expression
Assertion	mptfi	|- ( A e. Fin -> ( x e. A |-> B ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		funmpt	|- Fun ( x e. A |-> B )
2		funfn	|- ( Fun ( x e. A |-> B ) <-> ( x e. A |-> B ) Fn dom ( x e. A |-> B ) )
3	1 2	mpbi	|- ( x e. A |-> B ) Fn dom ( x e. A |-> B )
4		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
5	4	dmmptss	|- dom ( x e. A |-> B ) C_ A
6		ssfi	|- ( ( A e. Fin /\ dom ( x e. A |-> B ) C_ A ) -> dom ( x e. A |-> B ) e. Fin )
7	5 6	mpan2	|- ( A e. Fin -> dom ( x e. A |-> B ) e. Fin )
8		fnfi	|- ( ( ( x e. A |-> B ) Fn dom ( x e. A |-> B ) /\ dom ( x e. A |-> B ) e. Fin ) -> ( x e. A |-> B ) e. Fin )
9	3 7 8	sylancr	|- ( A e. Fin -> ( x e. A |-> B ) e. Fin )