This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )