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

Metamath Proof Explorer

Theorem imafi2

Description: The image by a finite set is finite. See also imafi . (Contributed by Thierry Arnoux, 25-Apr-2020)

Ref Expression
Assertion imafi2 ⊢ A ∈ Fin → A B ∈ Fin

Proof

Step Hyp Ref Expression
1 df-ima ⊢ A B = ran ⁡ A ↾ B
2 resss ⊢ A ↾ B ⊆ A
3 ssfi ⊢ A ∈ Fin ∧ A ↾ B ⊆ A → A ↾ B ∈ Fin
4 2 3 mpan2 ⊢ A ∈ Fin → A ↾ B ∈ Fin
5 rnfi ⊢ A ↾ B ∈ Fin → ran ⁡ A ↾ B ∈ Fin
6 4 5 syl ⊢ A ∈ Fin → ran ⁡ A ↾ B ∈ Fin
7 1 6 eqeltrid ⊢ A ∈ Fin → A B ∈ Fin