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 5932
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 6157, dffo3 6414, dffo4 6415, and dffo5 6416.

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 16785. (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 5924 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5921 . . 3 wff 𝐹 Fn 𝐴
63crn 5144 . . . 4 class ran 𝐹
76, 2wceq 1523 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 383 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 196 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  6149  foeq2  6150  foeq3  6151  nffo  6152  fof  6153  forn  6156  dffo2  6157  dffn4  6159  fores  6162  dff1o2  6180  dff1o3  6181  foimacnv  6192  foun  6193  fconst5  6512  dff1o6  6571  nvof1o  6576  f1oweALT  7194  fo1st  7230  fo2nd  7231  tposfo2  7420  fodomr  8152  f1finf1o  8228  unfilem2  8266  brwdom2  8519  harwdom  8536  infpwfien  8923  alephiso  8959  brdom3  9388  brdom5  9389  brdom4  9390  iunfo  9399  qnnen  14986  isfull2  16618  odf1o2  18034  cygctb  18339  qtopss  21566  qtopomap  21569  qtopcmap  21570  reeff1o  24246  efifo  24338  pjfoi  28690  bdayfo  31953  fobigcup  32132  fargshiftfo  41703
  Copyright terms: Public domain W3C validator