Definition df-fo 6579

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 6838, dffo3 7136, dffo4 7137, and dffo5 7138.

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 18155. (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 6571	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6568	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5701	. . . 4 class ran 𝐹
7	6, 2	wceq 1537	. . 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  6830  foeq2  6831  foeq3  6832  nffo  6833  fof  6834  forn  6837  dffo2  6838  dffn4  6840  fores  6844  dff1o2  6867  dff1o3  6868  foimacnv  6879  foun  6880  rescnvimafod  7107  fconst5  7243  dff1o6  7311  nvof1o  7316  f1oweALT  8013  fo1st  8050  fo2nd  8051  tposfo2  8290  fodomr  9194  f1finf1o  9333  f1finf1oOLD  9334  unfilem2  9372  fodomfir  9396  brwdom2  9642  harwdom  9660  infpwfien  10131  alephiso  10167  brdom3  10597  brdom5  10598  brdom4  10599  iunfo  10608  qnnen  16261  isfull2  17978  smndex2dnrinv  18950  odf1o2  19615  cygctb  19934  qtopss  23744  qtopomap  23747  qtopcmap  23748  reeff1o  26509  efifo  26607  bdayfo  27740  om2noseqfo  28322  pjfoi  31735  lvecendof1f1o  33646  fobigcup  35864  tfsconcatfo  43305  fundcmpsurinjlem2  47273  fargshiftfo  47316