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

Definition df-fo 5419
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 5616, dffo3 5843, dffo4 5844, and dffo5 5845. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fo  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wfo 5411 . 2  wff  F : A -onto-> B
53, 1wfn 5408 . . 3  wff  F  Fn  A
63crn 4838 . . . 4  class  ran  F
76, 2wceq 1649 . . 3  wff  ran  F  =  B
85, 7wa 359 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 177 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5608  foeq2  5609  foeq3  5610  nffo  5611  fof  5612  forn  5615  dffo2  5616  dffn4  5618  fores  5621  dff1o2  5638  dff1o3  5639  foimacnv  5651  foun  5652  fconst5  5908  fconstfv  5913  dff1o6  5972  f1oweALT  6033  fo1st  6325  fo2nd  6326  tposfo2  6461  fodomr  7217  f1finf1o  7294  unfilem2  7331  brwdom2  7497  harwdom  7514  infpwfien  7899  alephiso  7935  brdom3  8362  brdom5  8363  brdom4  8364  iunfo  8370  qnnen  12768  isfull2  14063  odf1o2  15162  cygctb  15456  qtopss  17700  qtopomap  17703  qtopcmap  17704  reeff1o  20316  efifo  20402  fargshiftfo  21578  pjfoi  23158  nvof1o  23993  ghomfo  25055  bdayfo  25543  fobigcup  25654
  Copyright terms: Public domain W3C validator