Metamath Proof Explorer

Theorem fof

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994)

Ref Expression
Assertion fof ⊢ F : A ⟶ onto B → F : A ⟶ B

Proof

Step Hyp Ref Expression
1 eqimss ⊢ ran ⁡ F = B → ran ⁡ F ⊆ B
2 1 anim2i ⊢ F Fn A ∧ ran ⁡ F = B → F Fn A ∧ ran ⁡ F ⊆ B
3 df-fo ⊢ F : A ⟶ onto B ↔ F Fn A ∧ ran ⁡ F = B
4 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
5 2 3 4 3imtr4i ⊢ F : A ⟶ onto B → F : A ⟶ B