Metamath Proof Explorer

Theorem mptfi

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

Ref Expression
Assertion mptfi ⊢ A ∈ Fin → x ∈ A ⟼ B ∈ Fin

Proof

Step Hyp Ref Expression
1 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
2 funfn ⊢ Fun ⁡ x ∈ A ⟼ B ↔ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B
3 1 2 mpbi ⊢ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B
4 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
5 4 dmmptss ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
6 ssfi ⊢ A ∈ Fin ∧ dom ⁡ x ∈ A ⟼ B ⊆ A → dom ⁡ x ∈ A ⟼ B ∈ Fin
7 5 6 mpan2 ⊢ A ∈ Fin → dom ⁡ x ∈ A ⟼ B ∈ Fin
8 fnfi ⊢ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ∈ Fin → x ∈ A ⟼ B ∈ Fin
9 3 7 8 sylancr ⊢ A ∈ Fin → x ∈ A ⟼ B ∈ Fin