Definition df-fo 6507

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 6765, dffo3 7057, dffo4 7058, and dffo5 7059.

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 17988. (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 6499	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6496	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5639	. . . 4 class ran 𝐹
7	6, 2	wceq 1541	. . 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  6757  foeq2  6758  foeq3  6759  nffo  6760  fof  6761  forn  6764  dffo2  6765  dffn4  6767  fores  6771  dff1o2  6794  dff1o3  6795  foimacnv  6806  foun  6807  rescnvimafod  7029  fconst5  7160  dff1o6  7226  nvof1o  7231  f1oweALT  7910  fo1st  7946  fo2nd  7947  tposfo2  8185  fodomr  9079  f1finf1o  9222  f1finf1oOLD  9223  unfilem2  9262  brwdom2  9518  harwdom  9536  infpwfien  10007  alephiso  10043  brdom3  10473  brdom5  10474  brdom4  10475  iunfo  10484  qnnen  16106  isfull2  17812  smndex2dnrinv  18739  odf1o2  19369  cygctb  19683  qtopss  23103  qtopomap  23106  qtopcmap  23107  reeff1o  25843  efifo  25940  bdayfo  27062  pjfoi  30708  fobigcup  34561  tfsconcatfo  41736  fundcmpsurinjlem2  45711  fargshiftfo  45754