Definition df-fo 6502

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 6754, dffo3 7052, dffo4 7053, and dffo5 7054.

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 18052. (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 6494	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6491	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5629	. . . 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  6746  foeq2  6747  foeq3  6748  nffo  6749  fof  6750  forn  6753  dffo2  6754  dffn4  6756  fores  6760  dff1o2  6783  dff1o3  6784  foimacnv  6795  foun  6796  rescnvimafod  7023  fconst5  7158  dff1o6  7227  nvof1o  7232  f1oweALT  7922  fo1st  7959  fo2nd  7960  tposfo2  8196  fodomr  9063  f1finf1o  9180  unfilem2  9213  fodomfir  9235  brwdom2  9485  harwdom  9503  infpwfien  9981  alephiso  10017  brdom3  10447  brdom5  10448  brdom4  10449  iunfo  10458  qnnen  16177  isfull2  17877  smndex2dnrinv  18883  odf1o2  19545  cygctb  19864  qtopss  23677  qtopomap  23680  qtopcmap  23681  reeff1o  26409  efifo  26508  bdayfo  27638  oniso  28260  om2noseqfo  28287  bdayn0sf1o  28359  pjfoi  31771  lvecendof1f1o  33774  fobigcup  36077  tfsconcatfo  43768  modelaxreplem1  45402  fundcmpsurinjlem2  47850  fargshiftfo  47893