Definition df-fo 6492

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 6744, dffo3 7041, dffo4 7042, and dffo5 7043.

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 17997. (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 6484	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6481	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5620	. . . 4 class ran 𝐹
7	6, 2	wceq 1541	. . 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  6736  foeq2  6737  foeq3  6738  nffo  6739  fof  6740  forn  6743  dffo2  6744  dffn4  6746  fores  6750  dff1o2  6773  dff1o3  6774  foimacnv  6785  foun  6786  rescnvimafod  7012  fconst5  7146  dff1o6  7215  nvof1o  7220  f1oweALT  7910  fo1st  7947  fo2nd  7948  tposfo2  8185  fodomr  9048  f1finf1o  9164  unfilem2  9197  fodomfir  9219  brwdom2  9466  harwdom  9484  infpwfien  9960  alephiso  9996  brdom3  10426  brdom5  10427  brdom4  10428  iunfo  10437  qnnen  16124  isfull2  17822  smndex2dnrinv  18825  odf1o2  19487  cygctb  19806  qtopss  23631  qtopomap  23634  qtopcmap  23635  reeff1o  26385  efifo  26484  bdayfo  27617  onsiso  28206  om2noseqfo  28229  bdayn0sf1o  28296  pjfoi  31685  lvecendof1f1o  33667  fobigcup  35963  tfsconcatfo  43460  modelaxreplem1  45095  fundcmpsurinjlem2  47523  fargshiftfo  47566