Definition df-fo 6238

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 6469, dffo3 6738, dffo4 6739, and dffo5 6740.

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 17181. (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 6230	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6227	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5451	. . . 4 class ran 𝐹
7	6, 2	wceq 1525	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 396	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 207	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6461  foeq2  6462  foeq3  6463  nffo  6464  fof  6465  forn  6468  dffo2  6469  dffn4  6471  fores  6475  dff1o2  6495  dff1o3  6496  foimacnv  6507  foun  6508  fconst5  6842  dff1o6  6904  nvof1o  6909  f1oweALT  7536  fo1st  7572  fo2nd  7573  tposfo2  7773  fodomr  8522  f1finf1o  8598  unfilem2  8636  brwdom2  8890  harwdom  8907  infpwfien  9341  alephiso  9377  brdom3  9803  brdom5  9804  brdom4  9805  iunfo  9814  qnnen  15403  isfull2  17014  odf1o2  18432  cygctb  18737  qtopss  22011  qtopomap  22014  qtopcmap  22015  reeff1o  24722  efifo  24816  pjfoi  29167  bdayfo  32793  fobigcup  32972  fargshiftfo  43106