Definition df-fo 6550

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 6810, dffo3 7104, dffo4 7105, and dffo5 7106.

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 18038. (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 6542	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 6539	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5678	. . . 4 class ran 𝐹
7	6, 2	wceq 1542	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 397	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6802  foeq2  6803  foeq3  6804  nffo  6805  fof  6806  forn  6809  dffo2  6810  dffn4  6812  fores  6816  dff1o2  6839  dff1o3  6840  foimacnv  6851  foun  6852  rescnvimafod  7076  fconst5  7207  dff1o6  7273  nvof1o  7278  f1oweALT  7959  fo1st  7995  fo2nd  7996  tposfo2  8234  fodomr  9128  f1finf1o  9271  f1finf1oOLD  9272  unfilem2  9311  brwdom2  9568  harwdom  9586  infpwfien  10057  alephiso  10093  brdom3  10523  brdom5  10524  brdom4  10525  iunfo  10534  qnnen  16156  isfull2  17862  smndex2dnrinv  18796  odf1o2  19441  cygctb  19760  qtopss  23219  qtopomap  23222  qtopcmap  23223  reeff1o  25959  efifo  26056  bdayfo  27180  pjfoi  30956  fobigcup  34872  tfsconcatfo  42093  fundcmpsurinjlem2  46067  fargshiftfo  46110