Definition df-fo 6519

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 6778, dffo3 7076, dffo4 7077, and dffo5 7078.

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 18056. (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 6511	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6508	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5641	. . . 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  6770  foeq2  6771  foeq3  6772  nffo  6773  fof  6774  forn  6777  dffo2  6778  dffn4  6780  fores  6784  dff1o2  6807  dff1o3  6808  foimacnv  6819  foun  6820  rescnvimafod  7047  fconst5  7182  dff1o6  7252  nvof1o  7257  f1oweALT  7953  fo1st  7990  fo2nd  7991  tposfo2  8230  fodomr  9097  f1finf1o  9222  f1finf1oOLD  9223  unfilem2  9261  fodomfir  9285  brwdom2  9532  harwdom  9550  infpwfien  10021  alephiso  10057  brdom3  10487  brdom5  10488  brdom4  10489  iunfo  10498  qnnen  16187  isfull2  17881  smndex2dnrinv  18848  odf1o2  19509  cygctb  19828  qtopss  23608  qtopomap  23611  qtopcmap  23612  reeff1o  26363  efifo  26462  bdayfo  27595  onsiso  28175  om2noseqfo  28198  bdayn0sf1o  28265  pjfoi  31638  lvecendof1f1o  33635  fobigcup  35883  tfsconcatfo  43325  modelaxreplem1  44961  fundcmpsurinjlem2  47390  fargshiftfo  47433