Definition df-fo 6568

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 6824, dffo3 7121, dffo4 7122, and dffo5 7123.

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 18141. (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 6560	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6557	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5689	. . . 4 class ran 𝐹
7	6, 2	wceq 1536	. . 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  6816  foeq2  6817  foeq3  6818  nffo  6819  fof  6820  forn  6823  dffo2  6824  dffn4  6826  fores  6830  dff1o2  6853  dff1o3  6854  foimacnv  6865  foun  6866  rescnvimafod  7092  fconst5  7225  dff1o6  7294  nvof1o  7299  f1oweALT  7995  fo1st  8032  fo2nd  8033  tposfo2  8272  fodomr  9166  f1finf1o  9302  f1finf1oOLD  9303  unfilem2  9341  fodomfir  9365  brwdom2  9610  harwdom  9628  infpwfien  10099  alephiso  10135  brdom3  10565  brdom5  10566  brdom4  10567  iunfo  10576  qnnen  16245  isfull2  17964  smndex2dnrinv  18940  odf1o2  19605  cygctb  19924  qtopss  23738  qtopomap  23741  qtopcmap  23742  reeff1o  26505  efifo  26603  bdayfo  27736  om2noseqfo  28318  pjfoi  31731  lvecendof1f1o  33660  fobigcup  35881  tfsconcatfo  43332  modelaxreplem1  44942  fundcmpsurinjlem2  47323  fargshiftfo  47366