Definition df-fo 6424

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 6676, dffo3 6960, dffo4 6961, and dffo5 6962.

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 17719. (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 6416	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6413	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5581	. . . 4 class ran 𝐹
7	6, 2	wceq 1539	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6668  foeq2  6669  foeq3  6670  nffo  6671  fof  6672  forn  6675  dffo2  6676  dffn4  6678  fores  6682  dff1o2  6705  dff1o3  6706  foimacnv  6717  foun  6718  rescnvimafod  6933  fconst5  7063  dff1o6  7128  nvof1o  7133  f1oweALT  7788  fo1st  7824  fo2nd  7825  tposfo2  8036  fodomr  8864  f1finf1o  8975  unfilem2  9009  brwdom2  9262  harwdom  9280  infpwfien  9749  alephiso  9785  brdom3  10215  brdom5  10216  brdom4  10217  iunfo  10226  qnnen  15850  isfull2  17543  smndex2dnrinv  18469  odf1o2  19093  cygctb  19408  qtopss  22774  qtopomap  22777  qtopcmap  22778  reeff1o  25511  efifo  25608  pjfoi  29966  bdayfo  33807  fobigcup  34129  fundcmpsurinjlem2  44739  fargshiftfo  44782