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

Metamath Proof Explorer

Theorem fisuppfi

Description: A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses fisuppfi.1 ⊢ φ → A ∈ Fin
fisuppfi.2 ⊢ φ → F : A ⟶ B
Assertion fisuppfi ⊢ φ → F -1 C ∈ Fin

Proof

Step Hyp Ref Expression
1 fisuppfi.1 ⊢ φ → A ∈ Fin
2 fisuppfi.2 ⊢ φ → F : A ⟶ B
3 cnvimass ⊢ F -1 C ⊆ dom ⁡ F
4 3 2 fssdm ⊢ φ → F -1 C ⊆ A
5 1 4 ssfid ⊢ φ → F -1 C ∈ Fin