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

Definition df-fo 5810
 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 6032, dffo3 6282, dffo4 6283, and dffo5 6284. 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 16561. (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 5802 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5799 . . 3 wff 𝐹 Fn 𝐴
63crn 5039 . . . 4 class ran 𝐹
76, 2wceq 1475 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 383 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 195 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  foeq1  6024  foeq2  6025  foeq3  6026  nffo  6027  fof  6028  forn  6031  dffo2  6032  dffn4  6034  fores  6037  dff1o2  6055  dff1o3  6056  foimacnv  6067  foun  6068  fconst5  6376  dff1o6  6431  nvof1o  6436  f1oweALT  7043  fo1st  7079  fo2nd  7080  tposfo2  7262  fodomr  7996  f1finf1o  8072  unfilem2  8110  brwdom2  8361  harwdom  8378  infpwfien  8768  alephiso  8804  brdom3  9231  brdom5  9232  brdom4  9233  iunfo  9240  qnnen  14781  isfull2  16394  odf1o2  17811  cygctb  18116  qtopss  21328  qtopomap  21331  qtopcmap  21332  reeff1o  24005  efifo  24097  fargshiftfo  26166  pjfoi  27946  bdayfo  31074  fobigcup  31177
 Copyright terms: Public domain W3C validator