Definition df-fo 6542

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 6796, dffo3 7097, dffo4 7098, and dffo5 7099.

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 18151. (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 6534	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6531	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5661	. . . 4 class ran 𝐹
7	6, 2	wceq 1569	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 400	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is used by:  foeq1  6788  foeq2  6789  foeq3  6790  nffo  6791  fof  6792  forn  6795  dffo2  6796  dffn4  6798  fores  6802  dff1o2  6826  dff1o3  6827  foimacnv  6838  foun  6839  rescnvimafod  7068  fconst5  7204  dff1o6  7273  nvof1o  7278  f1oweALT  7967  fo1st  8004  fo2nd  8005  tposfo2  8243  fodomr  9114  f1finf1o  9231  unfilem2  9264  fodomfir  9285  brwdom2  9533  harwdom  9551  infpwfien  10053  alephiso  10089  brdom3  10518  brdom5  10519  brdom4  10520  iunfo  10529  sgnfo  15143  qnnen  16275  isfull2  17976  smndex2dnrinv  18983  odf1o2  19649  cygctb  19968  qtopss  23883  qtopomap  23886  qtopcmap  23887  reeff1o  26621  efifo  26723  bdayfo  27852  oniso  28475  om2noseqfo  28502  bdayn0sf1o  28574  pjfoi  32066  lvecendof1f1o  34032  vonf1oonfo  35607  fobigcup  36398  tfsconcatfo  44098  modelaxreplem1  45715  fundcmpsurinjlem2  48176  fargshiftfo  48219