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 6103
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 6331, dffo3 6592, dffo4 6593, and dffo5 6594.

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 16938. (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 6095 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 6092 . . 3 wff 𝐹 Fn 𝐴
63crn 5312 . . . 4 class ran 𝐹
76, 2wceq 1637 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 384 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 197 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  6323  foeq2  6324  foeq3  6325  nffo  6326  fof  6327  forn  6330  dffo2  6331  dffn4  6333  fores  6336  dff1o2  6354  dff1o3  6355  foimacnv  6366  foun  6367  fconst5  6692  dff1o6  6751  nvof1o  6756  f1oweALT  7378  fo1st  7414  fo2nd  7415  tposfo2  7606  fodomr  8346  f1finf1o  8422  unfilem2  8460  brwdom2  8713  harwdom  8730  infpwfien  9164  alephiso  9200  brdom3  9631  brdom5  9632  brdom4  9633  iunfo  9642  qnnen  15158  isfull2  16771  odf1o2  18185  cygctb  18490  qtopss  21728  qtopomap  21731  qtopcmap  21732  reeff1o  24411  efifo  24504  pjfoi  28886  bdayfo  32144  fobigcup  32323  fargshiftfo  41947
  Copyright terms: Public domain W3C validator