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 ( 𝐴 ∈ 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 )