Definition df-fo 6517

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 6776, dffo3 7074, dffo4 7075, and dffo5 7076.

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 6509	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6506	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5639	. . . 4 class ran 𝐹
7	6, 2	wceq 1540	. . 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  6768  foeq2  6769  foeq3  6770  nffo  6771  fof  6772  forn  6775  dffo2  6776  dffn4  6778  fores  6782  dff1o2  6805  dff1o3  6806  foimacnv  6817  foun  6818  rescnvimafod  7045  fconst5  7180  dff1o6  7250  nvof1o  7255  f1oweALT  7951  fo1st  7988  fo2nd  7989  tposfo2  8228  fodomr  9092  f1finf1o  9216  f1finf1oOLD  9217  unfilem2  9255  fodomfir  9279  brwdom2  9526  harwdom  9544  infpwfien  10015  alephiso  10051  brdom3  10481  brdom5  10482  brdom4  10483  iunfo  10492  qnnen  16181  isfull2  17875  smndex2dnrinv  18842  odf1o2  19503  cygctb  19822  qtopss  23602  qtopomap  23605  qtopcmap  23606  reeff1o  26357  efifo  26456  bdayfo  27589  onsiso  28169  om2noseqfo  28192  bdayn0sf1o  28259  pjfoi  31632  lvecendof1f1o  33629  fobigcup  35888  tfsconcatfo  43332  modelaxreplem1  44968  fundcmpsurinjlem2  47397  fargshiftfo  47440