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

Definition df-fo 5463
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 5660, dffo3 5887, dffo4 5888, and dffo5 5889. (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 5455 . 2  wff  F : A -onto-> B
53, 1wfn 5452 . . 3  wff  F  Fn  A
63crn 4882 . . . 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  5652  foeq2  5653  foeq3  5654  nffo  5655  fof  5656  forn  5659  dffo2  5660  dffn4  5662  fores  5665  dff1o2  5682  dff1o3  5683  foimacnv  5695  foun  5696  fconst5  5952  fconstfv  5957  dff1o6  6016  f1oweALT  6077  fo1st  6369  fo2nd  6370  tposfo2  6505  fodomr  7261  f1finf1o  7338  unfilem2  7375  brwdom2  7544  harwdom  7561  infpwfien  7948  alephiso  7984  brdom3  8411  brdom5  8412  brdom4  8413  iunfo  8419  qnnen  12818  isfull2  14113  odf1o2  15212  cygctb  15506  qtopss  17752  qtopomap  17755  qtopcmap  17756  reeff1o  20368  efifo  20454  fargshiftfo  21630  pjfoi  23210  nvof1o  24045  ghomfo  25107  bdayfo  25635  fobigcup  25750
  Copyright terms: Public domain W3C validator