Definition df-fo 5894

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 6119, dffo3 6374, dffo4 6375, and dffo5 6376.

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 16738. (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 5886	. 2 wff 𝐹:𝐴–onto→𝐵
5	3, 1	wfn 5883	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5115	. . . 4 class ran 𝐹
7	6, 2	wceq 1483	. . 3 wff ran 𝐹 = 𝐵
8	5, 7	wa 384	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
9	4, 8	wb 196	1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

This definition is referenced by:  foeq1  6111  foeq2  6112  foeq3  6113  nffo  6114  fof  6115  forn  6118  dffo2  6119  dffn4  6121  fores  6124  dff1o2  6142  dff1o3  6143  foimacnv  6154  foun  6155  fconst5  6471  dff1o6  6531  nvof1o  6536  f1oweALT  7152  fo1st  7188  fo2nd  7189  tposfo2  7375  fodomr  8111  f1finf1o  8187  unfilem2  8225  brwdom2  8478  harwdom  8495  infpwfien  8885  alephiso  8921  brdom3  9350  brdom5  9351  brdom4  9352  iunfo  9361  qnnen  14942  isfull2  16571  odf1o2  17988  cygctb  18293  qtopss  21518  qtopomap  21521  qtopcmap  21522  reeff1o  24201  efifo  24293  pjfoi  28562  bdayfo  31828  fobigcup  32007  fargshiftfo  41378