MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fo Structured version   Visualization version   GIF version

Definition df-fo 5863
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 6086, dffo3 6340, dffo4 6341, and dffo5 6342.

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 16678. (Contributed by NM, 1-Aug-1994.)

Assertion
Ref Expression
df-fo (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wfo 5855 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5852 . . 3 wff 𝐹 Fn 𝐴
63crn 5085 . . . 4 class ran 𝐹
76, 2wceq 1480 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 384 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 196 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  6078  foeq2  6079  foeq3  6080  nffo  6081  fof  6082  forn  6085  dffo2  6086  dffn4  6088  fores  6091  dff1o2  6109  dff1o3  6110  foimacnv  6121  foun  6122  fconst5  6436  dff1o6  6496  nvof1o  6501  f1oweALT  7112  fo1st  7148  fo2nd  7149  tposfo2  7335  fodomr  8071  f1finf1o  8147  unfilem2  8185  brwdom2  8438  harwdom  8455  infpwfien  8845  alephiso  8881  brdom3  9310  brdom5  9311  brdom4  9312  iunfo  9321  qnnen  14886  isfull2  16511  odf1o2  17928  cygctb  18233  qtopss  21458  qtopomap  21461  qtopcmap  21462  reeff1o  24139  efifo  24231  pjfoi  28450  bdayfo  31591  fobigcup  31702  fargshiftfo  40706
  Copyright terms: Public domain W3C validator