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

Definition df-fo 5228
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 5421, dffo3 5637, dffo4 5638, and dffo5 5639. (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 5220 . 2  wff  F : A -onto-> B
53, 1wfn 5217 . . 3  wff  F  Fn  A
63crn 4690 . . . 4  class  ran  F
76, 2wceq 1624 . . 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  5413  foeq2  5414  foeq3  5415  nffo  5416  fof  5417  forn  5420  dffo2  5421  dffn4  5423  fores  5426  dff1o2  5443  dff1o3  5444  foimacnv  5456  foun  5457  fconst5  5693  fconstfv  5696  dff1o6  5753  f1oweALT  5813  fo1st  6101  fo2nd  6102  tposfo2  6219  fodomr  7008  f1finf1o  7082  unfilem2  7118  brwdom2  7283  harwdom  7300  infpwfien  7685  alephiso  7721  brdom3  8149  brdom5  8150  brdom4  8151  iunfo  8157  qnnen  12487  isfull2  13780  odf1o2  14879  cygctb  15173  qtopss  17401  qtopomap  17404  qtopcmap  17405  reeff1o  19818  efifo  19904  pjfoi  22275  nvof1o  23030  ghomfo  23403  axbday  23730  fobigcup  23849  dff1o6f  24491  trnij  25015
  Copyright terms: Public domain W3C validator