Definition df-fo 6567

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 6824, dffo3 7122, dffo4 7123, and dffo5 7124.

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 18133. (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 6559	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6556	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5686	. . . 4 class ran 𝐹
7	6, 2	wceq 1540	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 206	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6816  foeq2  6817  foeq3  6818  nffo  6819  fof  6820  forn  6823  dffo2  6824  dffn4  6826  fores  6830  dff1o2  6853  dff1o3  6854  foimacnv  6865  foun  6866  rescnvimafod  7093  fconst5  7226  dff1o6  7295  nvof1o  7300  f1oweALT  7997  fo1st  8034  fo2nd  8035  tposfo2  8274  fodomr  9168  f1finf1o  9305  f1finf1oOLD  9306  unfilem2  9344  fodomfir  9368  brwdom2  9613  harwdom  9631  infpwfien  10102  alephiso  10138  brdom3  10568  brdom5  10569  brdom4  10570  iunfo  10579  qnnen  16249  isfull2  17958  smndex2dnrinv  18928  odf1o2  19591  cygctb  19910  qtopss  23723  qtopomap  23726  qtopcmap  23727  reeff1o  26491  efifo  26589  bdayfo  27722  om2noseqfo  28304  pjfoi  31722  lvecendof1f1o  33684  fobigcup  35901  tfsconcatfo  43356  modelaxreplem1  44995  fundcmpsurinjlem2  47386  fargshiftfo  47429