Definition df-fo 6493

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 6745, dffo3 7043, dffo4 7044, and dffo5 7045.

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 18044. (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 6485	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6482	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5621	. . . 4 class ran 𝐹
7	6, 2	wceq 1542	. . 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  6737  foeq2  6738  foeq3  6739  nffo  6740  fof  6741  forn  6744  dffo2  6745  dffn4  6747  fores  6751  dff1o2  6774  dff1o3  6775  foimacnv  6786  foun  6787  rescnvimafod  7014  fconst5  7150  dff1o6  7219  nvof1o  7224  f1oweALT  7914  fo1st  7951  fo2nd  7952  tposfo2  8188  fodomr  9055  f1finf1o  9172  unfilem2  9205  fodomfir  9227  brwdom2  9477  harwdom  9495  infpwfien  9973  alephiso  10009  brdom3  10439  brdom5  10440  brdom4  10441  iunfo  10450  qnnen  16169  isfull2  17869  smndex2dnrinv  18875  odf1o2  19537  cygctb  19856  qtopss  23668  qtopomap  23671  qtopcmap  23672  reeff1o  26400  efifo  26499  bdayfo  27629  oniso  28251  om2noseqfo  28278  bdayn0sf1o  28350  pjfoi  31762  lvecendof1f1o  33765  fobigcup  36068  tfsconcatfo  43759  modelaxreplem1  45393  fundcmpsurinjlem2  47847  fargshiftfo  47890