Definition df-fo 6529

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 6784, dffo3 7085, dffo4 7086, and dffo5 7087.

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 18123. (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 6521	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6518	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5650	. . . 4 class ran 𝐹
7	6, 2	wceq 1562	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 399	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6776  foeq2  6777  foeq3  6778  nffo  6779  fof  6780  forn  6783  dffo2  6784  dffn4  6786  fores  6790  dff1o2  6814  dff1o3  6815  foimacnv  6826  foun  6827  rescnvimafod  7056  fconst5  7192  dff1o6  7261  nvof1o  7266  f1oweALT  7955  fo1st  7992  fo2nd  7993  tposfo2  8231  fodomr  9102  f1finf1o  9219  unfilem2  9252  fodomfir  9274  brwdom2  9523  harwdom  9541  infpwfien  10020  alephiso  10056  brdom3  10487  brdom5  10488  brdom4  10489  iunfo  10498  sgnfo  15114  qnnen  16247  isfull2  17948  smndex2dnrinv  18954  odf1o2  19615  cygctb  19934  qtopss  23777  qtopomap  23780  qtopcmap  23781  reeff1o  26512  efifo  26614  bdayfo  27743  oniso  28366  om2noseqfo  28393  bdayn0sf1o  28465  pjfoi  31908  lvecendof1f1o  33932  vonf1oonfo  35462  fobigcup  36253  tfsconcatfo  43925  modelaxreplem1  45559  fundcmpsurinjlem2  48010  fargshiftfo  48053