Definition df-fo 6386

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 6637, dffo3 6921, dffo4 6922, and dffo5 6923.

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 17594. (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 6378	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6375	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5552	. . . 4 class ran 𝐹
7	6, 2	wceq 1543	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 399	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6629  foeq2  6630  foeq3  6631  nffo  6632  fof  6633  forn  6636  dffo2  6637  dffn4  6639  fores  6643  dff1o2  6666  dff1o3  6667  foimacnv  6678  foun  6679  rescnvimafod  6894  fconst5  7021  dff1o6  7086  nvof1o  7091  f1oweALT  7745  fo1st  7781  fo2nd  7782  tposfo2  7991  fodomr  8797  f1finf1o  8902  unfilem2  8936  brwdom2  9189  harwdom  9207  infpwfien  9676  alephiso  9712  brdom3  10142  brdom5  10143  brdom4  10144  iunfo  10153  qnnen  15774  isfull2  17418  smndex2dnrinv  18342  odf1o2  18962  cygctb  19277  qtopss  22612  qtopomap  22615  qtopcmap  22616  reeff1o  25339  efifo  25436  pjfoi  29784  bdayfo  33617  fobigcup  33939  fundcmpsurinjlem2  44524  fargshiftfo  44567