Definition df-fo 6543

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 6797, dffo3 7098, dffo4 7099, and dffo5 7100.

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 18181. (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 6535	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6532	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5660	. . . 4 class ran 𝐹
7	6, 2	wceq 1570	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 401	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is used by:  foeq1  6789  foeq2  6790  foeq3  6791  nffo  6792  fof  6793  forn  6796  dffo2  6797  dffn4  6799  fores  6803  dff1o2  6827  dff1o3  6828  foimacnv  6839  foun  6840  rescnvimafod  7069  fconst5  7208  dff1o6  7279  nvof1o  7284  f1oweALT  7972  fo1st  8009  fo2nd  8010  tposfo2  8250  fodomr  9129  f1finf1o  9246  unfilem2  9279  fodomfir  9300  brwdom2  9548  harwdom  9566  infpwfien  10068  alephiso  10104  brdom3  10534  brdom5  10535  brdom4  10536  iunfo  10550  sgnfo  15174  qnnen  16305  isfull2  18006  smndex2dnrinv  19028  odf1o2  19701  cygctb  20020  qtopss  23942  qtopomap  23945  qtopcmap  23946  reeff1o  26680  efifo  26782  bdayfo  27911  oniso  28534  om2noseqfo  28561  bdayn0sf1o  28633  pjfoi  32170  lvecendof1f1o  34130  vonf1oonfo  35699  fobigcup  36464  tfsconcatfo  44171  modelaxreplem1  45788  fundcmpsurinjlem2  48286  fargshiftfo  48329