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 5795
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 6016, dffo3 6266, dffo4 6267, and dffo5 6268.

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 16509. (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 5787 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5784 . . 3 wff 𝐹 Fn 𝐴
63crn 5028 . . . 4 class ran 𝐹
76, 2wceq 1474 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 382 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 194 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  6008  foeq2  6009  foeq3  6010  nffo  6011  fof  6012  forn  6015  dffo2  6016  dffn4  6018  fores  6021  dff1o2  6039  dff1o3  6040  foimacnv  6051  foun  6052  fconst5  6353  dff1o6  6408  nvof1o  6413  f1oweALT  7020  fo1st  7056  fo2nd  7057  tposfo2  7239  fodomr  7973  f1finf1o  8049  unfilem2  8087  brwdom2  8338  harwdom  8355  infpwfien  8745  alephiso  8781  brdom3  9208  brdom5  9209  brdom4  9210  iunfo  9217  qnnen  14729  isfull2  16342  odf1o2  17759  cygctb  18064  qtopss  21275  qtopomap  21278  qtopcmap  21279  reeff1o  23949  efifo  24041  fargshiftfo  25959  pjfoi  27739  bdayfo  30867  fobigcup  30970
  Copyright terms: Public domain W3C validator