Definition df-fo 6492

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 6744, dffo3 7040, dffo4 7041, and dffo5 7042.

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 18013. (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 6484	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6481	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5624	. . . 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  6736  foeq2  6737  foeq3  6738  nffo  6739  fof  6740  forn  6743  dffo2  6744  dffn4  6746  fores  6750  dff1o2  6773  dff1o3  6774  foimacnv  6785  foun  6786  rescnvimafod  7011  fconst5  7146  dff1o6  7216  nvof1o  7221  f1oweALT  7914  fo1st  7951  fo2nd  7952  tposfo2  8189  fodomr  9052  f1finf1o  9174  f1finf1oOLD  9175  unfilem2  9213  fodomfir  9237  brwdom2  9484  harwdom  9502  infpwfien  9975  alephiso  10011  brdom3  10441  brdom5  10442  brdom4  10443  iunfo  10452  qnnen  16140  isfull2  17838  smndex2dnrinv  18807  odf1o2  19470  cygctb  19789  qtopss  23618  qtopomap  23621  qtopcmap  23622  reeff1o  26373  efifo  26472  bdayfo  27605  onsiso  28192  om2noseqfo  28215  bdayn0sf1o  28282  pjfoi  31665  lvecendof1f1o  33605  fobigcup  35873  tfsconcatfo  43316  modelaxreplem1  44952  fundcmpsurinjlem2  47384  fargshiftfo  47427