Definition df-fo 6512

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 6767, dffo3 7068, dffo4 7069, and dffo5 7070.

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 18093. (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 6504	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6501	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5637	. . . 4 class ran 𝐹
7	6, 2	wceq 1550	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 398	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6759  foeq2  6760  foeq3  6761  nffo  6762  fof  6763  forn  6766  dffo2  6767  dffn4  6769  fores  6773  dff1o2  6797  dff1o3  6798  foimacnv  6809  foun  6810  rescnvimafod  7039  fconst5  7175  dff1o6  7244  nvof1o  7249  f1oweALT  7938  fo1st  7975  fo2nd  7976  tposfo2  8213  fodomr  9085  f1finf1o  9202  unfilem2  9235  fodomfir  9257  brwdom2  9507  harwdom  9525  infpwfien  10004  alephiso  10040  brdom3  10471  brdom5  10472  brdom4  10473  iunfo  10482  qnnen  16217  isfull2  17918  smndex2dnrinv  18924  odf1o2  19585  cygctb  19904  qtopss  23744  qtopomap  23747  qtopcmap  23748  reeff1o  26476  efifo  26578  bdayfo  27707  oniso  28330  om2noseqfo  28357  bdayn0sf1o  28429  pjfoi  31841  lvecendof1f1o  33874  fobigcup  36186  tfsconcatfo  43858  modelaxreplem1  45492  fundcmpsurinjlem2  47943  fargshiftfo  47986