Definition df-fo 5810

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 6032, dffo3 6282, dffo4 6283, and dffo5 6284.

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 16561. (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 5802	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5799	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5039	. . . 4 class ran 𝐹
7	6, 2	wceq 1475	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 383	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 195	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6024  foeq2  6025  foeq3  6026  nffo  6027  fof  6028  forn  6031  dffo2  6032  dffn4  6034  fores  6037  dff1o2  6055  dff1o3  6056  foimacnv  6067  foun  6068  fconst5  6376  dff1o6  6431  nvof1o  6436  f1oweALT  7043  fo1st  7079  fo2nd  7080  tposfo2  7262  fodomr  7996  f1finf1o  8072  unfilem2  8110  brwdom2  8361  harwdom  8378  infpwfien  8768  alephiso  8804  brdom3  9231  brdom5  9232  brdom4  9233  iunfo  9240  qnnen  14781  isfull2  16394  odf1o2  17811  cygctb  18116  qtopss  21328  qtopomap  21331  qtopcmap  21332  reeff1o  24005  efifo  24097  fargshiftfo  26166  pjfoi  27946  bdayfo  31074  fobigcup  31177