Definition df-fo 6485

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 6743, dffo3 7034, dffo4 7035, and dffo5 7036.

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

Assertion

Ref	Expression
df-fo	⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

Detailed syntax breakdown of Definition df-fo

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wfo 6477	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6474	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5621	. . . 4 class ran 𝐹
7	6, 2	wceq 1540	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 396	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6735  foeq2  6736  foeq3  6737  nffo  6738  fof  6739  forn  6742  dffo2  6743  dffn4  6745  fores  6749  dff1o2  6772  dff1o3  6773  foimacnv  6784  foun  6785  rescnvimafod  7007  fconst5  7137  dff1o6  7203  nvof1o  7208  f1oweALT  7883  fo1st  7919  fo2nd  7920  tposfo2  8135  fodomr  8993  f1finf1o  9136  f1finf1oOLD  9137  unfilem2  9176  brwdom2  9430  harwdom  9448  infpwfien  9919  alephiso  9955  brdom3  10385  brdom5  10386  brdom4  10387  iunfo  10396  qnnen  16021  isfull2  17724  smndex2dnrinv  18650  odf1o2  19274  cygctb  19588  qtopss  22972  qtopomap  22975  qtopcmap  22976  reeff1o  25712  efifo  25809  bdayfo  26931  pjfoi  30353  fobigcup  34298  fundcmpsurinjlem2  45210  fargshiftfo  45253