Definition df-fo 6561

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 6819, dffo3 7123, dffo4 7124, and dffo5 7125.

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 18289. (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 6553	. 2 wff 𝐹:𝐴⟶onto𝐵
5	3, 1	wfn 6550	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5656	. . . 4 class ran 𝐹
7	6, 2	wceq 1570	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 401	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is used by:  foeq1  6811  foeq2  6812  foeq3  6813  nffo  6814  fof  6815  forn  6818  dffo2  6819  dffn4  6821  fores  6825  dff1o2  6849  dff1o3  6850  foimacnv  6861  foun  6862  rescnvimafod  7094  fconst5  7232  dff1o6  7303  nvof1o  7308  f1oweALT  8005  fo1st  8042  fo2nd  8043  tposfo2  8291  fodomr  9172  f1finf1o  9289  unfilem2  9323  fodomfir  9344  brwdom2  9591  harwdom  9609  infpwfien  10165  alephiso  10201  brdom3  10631  brdom5  10632  brdom4  10633  iunfo  10647  sgnfo  15278  qnnen  16407  isfull2  18114  smndex2dnrinv  19140  odf1o2  19814  cygctb  20133  qtopss  24061  qtopomap  24064  qtopcmap  24065  reeff1o  26801  efifo  26902  bdayfo  28061  oniso  28684  om2noseqfo  28711  bdayn0sf1o  28783  pjfoi  32332  lvecendof1f1o  34332  vonf1oonfo  36048  fobigcup  36839  tfsconcatfo  44535  modelaxreplem1  46161  fundcmpsurinjlem2  48684  fargshiftfo  48727