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

Definition df-fo 6331
 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 6570, dffo3 6846, dffo4 6847, and dffo5 6848. 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 17343. (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 6323 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 6320 . . 3 wff 𝐹 Fn 𝐴
63crn 5521 . . . 4 class ran 𝐹
76, 2wceq 1538 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 399 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 209 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  foeq1  6562  foeq2  6563  foeq3  6564  nffo  6565  fof  6566  forn  6569  dffo2  6570  dffn4  6572  fores  6576  dff1o2  6596  dff1o3  6597  foimacnv  6608  foun  6609  fconst5  6946  dff1o6  7011  nvof1o  7016  f1oweALT  7658  fo1st  7694  fo2nd  7695  tposfo2  7901  fodomr  8655  f1finf1o  8732  unfilem2  8770  brwdom2  9024  harwdom  9042  infpwfien  9476  alephiso  9512  brdom3  9942  brdom5  9943  brdom4  9944  iunfo  9953  qnnen  15561  isfull2  17176  smndex2dnrinv  18075  odf1o2  18694  cygctb  19009  qtopss  22330  qtopomap  22333  qtopcmap  22334  reeff1o  25052  efifo  25149  pjfoi  29496  bdayfo  33310  fobigcup  33489  fundcmpsurinjlem2  43959  fargshiftfo  44002
 Copyright terms: Public domain W3C validator