Definition df-fo 6533

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

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 18224. (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 6525	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6522	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5648	. . . 4 class ran 𝐹
7	6, 2	wceq 1570	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 401	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is used by:  foeq1  6780  foeq2  6781  foeq3  6782  nffo  6783  fof  6784  forn  6787  dffo2  6788  dffn4  6790  fores  6794  dff1o2  6818  dff1o3  6819  foimacnv  6830  foun  6831  rescnvimafod  7061  fconst5  7200  dff1o6  7271  nvof1o  7276  f1oweALT  7967  fo1st  8004  fo2nd  8005  tposfo2  8244  fodomr  9125  f1finf1o  9242  unfilem2  9276  fodomfir  9297  brwdom2  9545  harwdom  9563  infpwfien  10112  alephiso  10148  brdom3  10578  brdom5  10579  brdom4  10580  iunfo  10594  sgnfo  15219  qnnen  16348  isfull2  18049  smndex2dnrinv  19075  odf1o2  19748  cygctb  20067  qtopss  23995  qtopomap  23998  qtopcmap  23999  reeff1o  26737  efifo  26838  bdayfo  27967  oniso  28590  om2noseqfo  28617  bdayn0sf1o  28689  pjfoi  32238  lvecendof1f1o  34198  vonf1oonfo  35819  fobigcup  36584  tfsconcatfo  44288  modelaxreplem1  45905  fundcmpsurinjlem2  48403  fargshiftfo  48446