Definition df-fo 6544

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 6800, dffo3 7102, dffo4 7103, and dffo5 7104.

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 18263. (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 6536	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6533	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5651	. . . 4 class ran 𝐹
7	6, 2	wceq 1569	. . 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  6792  foeq2  6793  foeq3  6794  nffo  6795  fof  6796  forn  6799  dffo2  6800  dffn4  6802  fores  6806  dff1o2  6830  dff1o3  6831  foimacnv  6842  foun  6843  rescnvimafod  7073  fconst5  7212  dff1o6  7283  nvof1o  7288  f1oweALT  7984  fo1st  8021  fo2nd  8022  tposfo2  8266  fodomr  9147  f1finf1o  9264  unfilem2  9298  fodomfir  9319  brwdom2  9567  harwdom  9585  infpwfien  10141  alephiso  10177  brdom3  10607  brdom5  10608  brdom4  10609  iunfo  10623  sgnfo  15252  qnnen  16381  isfull2  18088  smndex2dnrinv  19114  odf1o2  19787  cygctb  20106  qtopss  24034  qtopomap  24037  qtopcmap  24038  reeff1o  26774  efifo  26875  bdayfo  28034  oniso  28657  om2noseqfo  28684  bdayn0sf1o  28756  pjfoi  32305  lvecendof1f1o  34307  vonf1oonfo  35940  fobigcup  36704  tfsconcatfo  44387  modelaxreplem1  46010  fundcmpsurinjlem2  48523  fargshiftfo  48566