Definition df-fo 6361

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 6594, dffo3 6868, dffo4 6869, and dffo5 6870.

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 17348. (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 6353	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6350	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5556	. . . 4 class ran 𝐹
7	6, 2	wceq 1537	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 398	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6586  foeq2  6587  foeq3  6588  nffo  6589  fof  6590  forn  6593  dffo2  6594  dffn4  6596  fores  6600  dff1o2  6620  dff1o3  6621  foimacnv  6632  foun  6633  fconst5  6968  dff1o6  7032  nvof1o  7037  f1oweALT  7673  fo1st  7709  fo2nd  7710  tposfo2  7915  fodomr  8668  f1finf1o  8745  unfilem2  8783  brwdom2  9037  harwdom  9054  infpwfien  9488  alephiso  9524  brdom3  9950  brdom5  9951  brdom4  9952  iunfo  9961  qnnen  15566  isfull2  17181  smndex2dnrinv  18080  odf1o2  18698  cygctb  19012  qtopss  22323  qtopomap  22326  qtopcmap  22327  reeff1o  25035  efifo  25131  pjfoi  29480  bdayfo  33182  fobigcup  33361  fundcmpsurinjlem2  43608  fargshiftfo  43651