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

Definition df-fo 5489
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 5686, dffo3 5913, dffo4 5914, and dffo5 5915. (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 5481 . 2  wff  F : A -onto-> B
53, 1wfn 5478 . . 3  wff  F  Fn  A
63crn 4908 . . . 4  class  ran  F
76, 2wceq 1653 . . 3  wff  ran  F  =  B
85, 7wa 360 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 178 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5678  foeq2  5679  foeq3  5680  nffo  5681  fof  5682  forn  5685  dffo2  5686  dffn4  5688  fores  5691  dff1o2  5708  dff1o3  5709  foimacnv  5721  foun  5722  fconst5  5978  fconstfv  5983  dff1o6  6042  f1oweALT  6103  fo1st  6395  fo2nd  6396  tposfo2  6531  fodomr  7287  f1finf1o  7364  unfilem2  7401  brwdom2  7570  harwdom  7587  infpwfien  7974  alephiso  8010  brdom3  8437  brdom5  8438  brdom4  8439  iunfo  8445  qnnen  12844  isfull2  14139  odf1o2  15238  cygctb  15532  qtopss  17778  qtopomap  17781  qtopcmap  17782  reeff1o  20394  efifo  20480  fargshiftfo  21656  pjfoi  23236  nvof1o  24071  ghomfo  25133  bdayfo  25661  fobigcup  25776
  Copyright terms: Public domain W3C validator