# Metamath Proof Explorer

## Definition df-fo

Description: Define an onto function. Definition 6.15(4) of TakeutiZaring p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 , dffo3 , dffo4 , and dffo5 .

An onto function is also called a "surjection" or a "surjective function", F : A -onto-> B can be read as " F is a surjection from A onto B ". Surjections are precisely the epimorphisms in the category SetCat of sets and set functions, see setcepi . (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion df-fo ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ${class}{F}$
1 cA ${class}{A}$
2 cB ${class}{B}$
3 1 2 0 wfo ${wff}{F}:{A}\underset{onto}{⟶}{B}$
4 0 1 wfn ${wff}{F}Fn{A}$
5 0 crn ${class}\mathrm{ran}{F}$
6 5 2 wceq ${wff}\mathrm{ran}{F}={B}$
7 4 6 wa ${wff}\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)$
8 3 7 wb ${wff}\left({F}:{A}\underset{onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)\right)$