Definition df-fo 6542

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 6796, dffo3 7097, dffo4 7098, and dffo5 7099.

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 18144. (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 6534	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6531	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5662	. . . 4 class ran 𝐹
7	6, 2	wceq 1568	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 400	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6788  foeq2  6789  foeq3  6790  nffo  6791  fof  6792  forn  6795  dffo2  6796  dffn4  6798  fores  6802  dff1o2  6826  dff1o3  6827  foimacnv  6838  foun  6839  rescnvimafod  7068  fconst5  7204  dff1o6  7273  nvof1o  7278  f1oweALT  7968  fo1st  8005  fo2nd  8006  tposfo2  8244  fodomr  9115  f1finf1o  9232  unfilem2  9265  fodomfir  9286  brwdom2  9534  harwdom  9552  infpwfien  10045  alephiso  10081  brdom3  10511  brdom5  10512  brdom4  10513  iunfo  10522  sgnfo  15135  qnnen  16268  isfull2  17969  smndex2dnrinv  18976  odf1o2  19642  cygctb  19961  qtopss  23851  qtopomap  23854  qtopcmap  23855  reeff1o  26586  efifo  26688  bdayfo  27817  oniso  28440  om2noseqfo  28467  bdayn0sf1o  28539  pjfoi  32021  lvecendof1f1o  33989  vonf1oonfo  35553  fobigcup  36344  tfsconcatfo  44018  modelaxreplem1  45635  fundcmpsurinjlem2  48093  fargshiftfo  48136