Definition df-fo 6443

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 6701, dffo3 6987, dffo4 6988, and dffo5 6989.

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 17812. (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 6435	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6432	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5591	. . . 4 class ran 𝐹
7	6, 2	wceq 1539	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 396	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6693  foeq2  6694  foeq3  6695  nffo  6696  fof  6697  forn  6700  dffo2  6701  dffn4  6703  fores  6707  dff1o2  6730  dff1o3  6731  foimacnv  6742  foun  6743  rescnvimafod  6960  fconst5  7090  dff1o6  7156  nvof1o  7161  f1oweALT  7824  fo1st  7860  fo2nd  7861  tposfo2  8074  fodomr  8924  f1finf1o  9055  unfilem2  9088  brwdom2  9341  harwdom  9359  infpwfien  9827  alephiso  9863  brdom3  10293  brdom5  10294  brdom4  10295  iunfo  10304  qnnen  15931  isfull2  17636  smndex2dnrinv  18563  odf1o2  19187  cygctb  19502  qtopss  22875  qtopomap  22878  qtopcmap  22879  reeff1o  25615  efifo  25712  pjfoi  30074  bdayfo  33889  fobigcup  34211  fundcmpsurinjlem2  44862  fargshiftfo  44905