Definition df-fo 6494

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 6746, dffo3 7046, dffo4 7047, and dffo5 7048.

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 18050. (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 6486	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6483	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5621	. . . 4 class ran 𝐹
7	6, 2	wceq 1548	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 397	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6738  foeq2  6739  foeq3  6740  nffo  6741  fof  6742  forn  6745  dffo2  6746  dffn4  6748  fores  6752  dff1o2  6775  dff1o3  6776  foimacnv  6787  foun  6788  rescnvimafod  7017  fconst5  7153  dff1o6  7222  nvof1o  7227  f1oweALT  7916  fo1st  7953  fo2nd  7954  tposfo2  8191  fodomr  9060  f1finf1o  9177  unfilem2  9210  fodomfir  9232  brwdom2  9482  harwdom  9500  infpwfien  9979  alephiso  10015  brdom3  10446  brdom5  10447  brdom4  10448  iunfo  10457  qnnen  16175  isfull2  17875  smndex2dnrinv  18881  odf1o2  19542  cygctb  19861  qtopss  23701  qtopomap  23704  qtopcmap  23705  reeff1o  26433  efifo  26532  bdayfo  27661  oniso  28283  om2noseqfo  28310  bdayn0sf1o  28382  pjfoi  31794  lvecendof1f1o  33827  fobigcup  36139  tfsconcatfo  43801  modelaxreplem1  45435  fundcmpsurinjlem2  47886  fargshiftfo  47929