Definition df-fo 6508

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 6760, dffo3 7058, dffo4 7059, and dffo5 7060.

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 18026. (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 6500	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6497	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5635	. . . 4 class ran 𝐹
7	6, 2	wceq 1542	. . 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  6752  foeq2  6753  foeq3  6754  nffo  6755  fof  6756  forn  6759  dffo2  6760  dffn4  6762  fores  6766  dff1o2  6789  dff1o3  6790  foimacnv  6801  foun  6802  rescnvimafod  7029  fconst5  7164  dff1o6  7233  nvof1o  7238  f1oweALT  7928  fo1st  7965  fo2nd  7966  tposfo2  8203  fodomr  9070  f1finf1o  9187  unfilem2  9220  fodomfir  9242  brwdom2  9492  harwdom  9510  infpwfien  9986  alephiso  10022  brdom3  10452  brdom5  10453  brdom4  10454  iunfo  10463  qnnen  16152  isfull2  17851  smndex2dnrinv  18857  odf1o2  19519  cygctb  19838  qtopss  23676  qtopomap  23679  qtopcmap  23680  reeff1o  26430  efifo  26529  bdayfo  27662  oniso  28284  om2noseqfo  28311  bdayn0sf1o  28383  pjfoi  31797  lvecendof1f1o  33817  fobigcup  36120  tfsconcatfo  43729  modelaxreplem1  45363  fundcmpsurinjlem2  47788  fargshiftfo  47831