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

Definition df-fo 5587
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 5792, dffo3 6029, dffo4 6030, and dffo5 6031. (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 5579 . 2  wff  F : A -onto-> B
53, 1wfn 5576 . . 3  wff  F  Fn  A
63crn 4995 . . . 4  class  ran  F
76, 2wceq 1374 . . 3  wff  ran  F  =  B
85, 7wa 369 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 184 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  5784  foeq2  5785  foeq3  5786  nffo  5787  fof  5788  forn  5791  dffo2  5792  dffn4  5794  fores  5797  dff1o2  5814  dff1o3  5815  foimacnv  5826  foun  5827  fconst5  6111  fconstfv  6116  dff1o6  6162  nvof1o  6167  f1oweALT  6760  fo1st  6796  fo2nd  6797  tposfo2  6970  fodomr  7660  f1finf1o  7738  unfilem2  7776  brwdom2  7990  harwdom  8007  infpwfien  8434  alephiso  8470  brdom3  8897  brdom5  8898  brdom4  8899  iunfo  8905  qnnen  13799  isfull2  15129  odf1o2  16384  cygctb  16680  qtopss  19946  qtopomap  19949  qtopcmap  19950  reeff1o  22571  efifo  22662  fargshiftfo  24302  pjfoi  26285  ghomfo  28494  bdayfo  29000  fobigcup  29115
  Copyright terms: Public domain W3C validator