Definition df-fo 6487

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 6739, dffo3 7035, dffo4 7036, and dffo5 7037.

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 17992. (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 6479	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6476	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5617	. . . 4 class ran 𝐹
7	6, 2	wceq 1541	. . 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  6731  foeq2  6732  foeq3  6733  nffo  6734  fof  6735  forn  6738  dffo2  6739  dffn4  6741  fores  6745  dff1o2  6768  dff1o3  6769  foimacnv  6780  foun  6781  rescnvimafod  7006  fconst5  7140  dff1o6  7209  nvof1o  7214  f1oweALT  7904  fo1st  7941  fo2nd  7942  tposfo2  8179  fodomr  9041  f1finf1o  9157  unfilem2  9190  fodomfir  9212  brwdom2  9459  harwdom  9477  infpwfien  9950  alephiso  9986  brdom3  10416  brdom5  10417  brdom4  10418  iunfo  10427  qnnen  16119  isfull2  17817  smndex2dnrinv  18820  odf1o2  19483  cygctb  19802  qtopss  23628  qtopomap  23631  qtopcmap  23632  reeff1o  26382  efifo  26481  bdayfo  27614  onsiso  28203  om2noseqfo  28226  bdayn0sf1o  28293  pjfoi  31678  lvecendof1f1o  33641  fobigcup  35933  tfsconcatfo  43375  modelaxreplem1  45010  fundcmpsurinjlem2  47429  fargshiftfo  47472