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

Metamath Proof Explorer

Theorem f1vrnfibi

Description: A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi . (Contributed by AV, 10-Jan-2020)

Ref Expression
Assertion f1vrnfibi ⊢ F ∈ V ∧ F : A ⟶ 1-1 B → F ∈ Fin ↔ ran ⁡ F ∈ Fin

Proof

Step Hyp Ref Expression
1 f1dm ⊢ F : A ⟶ 1-1 B → dom ⁡ F = A
2 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
3 eleq1 ⊢ A = dom ⁡ F → A ∈ V ↔ dom ⁡ F ∈ V
4 3 eqcoms ⊢ dom ⁡ F = A → A ∈ V ↔ dom ⁡ F ∈ V
5 2 4 imbitrrid ⊢ dom ⁡ F = A → F ∈ V → A ∈ V
6 1 5 syl ⊢ F : A ⟶ 1-1 B → F ∈ V → A ∈ V
7 6 impcom ⊢ F ∈ V ∧ F : A ⟶ 1-1 B → A ∈ V
8 f1dmvrnfibi ⊢ A ∈ V ∧ F : A ⟶ 1-1 B → F ∈ Fin ↔ ran ⁡ F ∈ Fin
9 7 8 sylancom ⊢ F ∈ V ∧ F : A ⟶ 1-1 B → F ∈ Fin ↔ ran ⁡ F ∈ Fin