Definition df-fo 6536

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 6793, dffo3 7091, dffo4 7092, and dffo5 7093.

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 18099. (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 6528	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6525	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5655	. . . 4 class ran 𝐹
7	6, 2	wceq 1540	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 206	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6785  foeq2  6786  foeq3  6787  nffo  6788  fof  6789  forn  6792  dffo2  6793  dffn4  6795  fores  6799  dff1o2  6822  dff1o3  6823  foimacnv  6834  foun  6835  rescnvimafod  7062  fconst5  7197  dff1o6  7267  nvof1o  7272  f1oweALT  7969  fo1st  8006  fo2nd  8007  tposfo2  8246  fodomr  9140  f1finf1o  9275  f1finf1oOLD  9276  unfilem2  9314  fodomfir  9338  brwdom2  9585  harwdom  9603  infpwfien  10074  alephiso  10110  brdom3  10540  brdom5  10541  brdom4  10542  iunfo  10551  qnnen  16229  isfull2  17924  smndex2dnrinv  18891  odf1o2  19552  cygctb  19871  qtopss  23651  qtopomap  23654  qtopcmap  23655  reeff1o  26407  efifo  26506  bdayfo  27639  om2noseqfo  28221  pjfoi  31630  lvecendof1f1o  33619  fobigcup  35864  tfsconcatfo  43314  modelaxreplem1  44951  fundcmpsurinjlem2  47361  fargshiftfo  47404