Definition df-fo 6499

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 6751, dffo3 7049, dffo4 7050, and dffo5 7051.

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 18016. (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 6491	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6488	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5626	. . . 4 class ran 𝐹
7	6, 2	wceq 1542	. . 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  6743  foeq2  6744  foeq3  6745  nffo  6746  fof  6747  forn  6750  dffo2  6751  dffn4  6753  fores  6757  dff1o2  6780  dff1o3  6781  foimacnv  6792  foun  6793  rescnvimafod  7020  fconst5  7154  dff1o6  7223  nvof1o  7228  f1oweALT  7918  fo1st  7955  fo2nd  7956  tposfo2  8193  fodomr  9060  f1finf1o  9177  unfilem2  9210  fodomfir  9232  brwdom2  9482  harwdom  9500  infpwfien  9976  alephiso  10012  brdom3  10442  brdom5  10443  brdom4  10444  iunfo  10453  qnnen  16142  isfull2  17841  smndex2dnrinv  18844  odf1o2  19506  cygctb  19825  qtopss  23663  qtopomap  23666  qtopcmap  23667  reeff1o  26417  efifo  26516  bdayfo  27649  oniso  28271  om2noseqfo  28298  bdayn0sf1o  28370  pjfoi  31782  lvecendof1f1o  33792  fobigcup  36094  tfsconcatfo  43652  modelaxreplem1  45286  fundcmpsurinjlem2  47712  fargshiftfo  47755