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

Metamath Proof Explorer

Theorem f1ores

Description: The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998)

Ref Expression
Assertion f1ores ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F ↾ C : C ⟶ 1-1 onto F C

Proof

Step Hyp Ref Expression
1 f1ssres ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F ↾ C : C ⟶ 1-1 B
2 f1f1orn ⊢ F ↾ C : C ⟶ 1-1 B → F ↾ C : C ⟶ 1-1 onto ran ⁡ F ↾ C
3 1 2 syl ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F ↾ C : C ⟶ 1-1 onto ran ⁡ F ↾ C
4 df-ima ⊢ F C = ran ⁡ F ↾ C
5 f1oeq3 ⊢ F C = ran ⁡ F ↾ C → F ↾ C : C ⟶ 1-1 onto F C ↔ F ↾ C : C ⟶ 1-1 onto ran ⁡ F ↾ C
6 4 5 ax-mp ⊢ F ↾ C : C ⟶ 1-1 onto F C ↔ F ↾ C : C ⟶ 1-1 onto ran ⁡ F ↾ C
7 3 6 sylibr ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F ↾ C : C ⟶ 1-1 onto F C