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

Definition df-fo 5550
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 5757, dffo3 5996, dffo4 5997, and dffo5 5998. (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 5542 . 2  wff  F : A -onto-> B
53, 1wfn 5539 . . 3  wff  F  Fn  A
63crn 4797 . . . 4  class  ran  F
76, 2wceq 1437 . . 3  wff  ran  F  =  B
85, 7wa 370 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 187 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  5749  foeq2  5750  foeq3  5751  nffo  5752  fof  5753  forn  5756  dffo2  5757  dffn4  5759  fores  5762  dff1o2  5779  dff1o3  5780  foimacnv  5791  foun  5792  fconst5  6081  fconstfvOLD  6086  dff1o6  6133  nvof1o  6138  f1oweALT  6735  fo1st  6771  fo2nd  6772  tposfo2  6951  fodomr  7676  f1finf1o  7751  unfilem2  7789  brwdom2  8041  harwdom  8058  infpwfien  8444  alephiso  8480  brdom3  8907  brdom5  8908  brdom4  8909  iunfo  8915  qnnen  14209  isfull2  15759  odf1o2  17165  cygctb  17469  qtopss  20672  qtopomap  20675  qtopcmap  20676  reeff1o  23344  efifo  23438  fargshiftfo  25308  pjfoi  27298  ghomfo  30261  bdayfo  30513  fobigcup  30616
  Copyright terms: Public domain W3C validator