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

Definition df-fo 5607
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 5820, dffo3 6060, dffo4 6061, and dffo5 6062. (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 5599 . 2  wff  F : A -onto-> B
53, 1wfn 5596 . . 3  wff  F  Fn  A
63crn 4854 . . . 4  class  ran  F
76, 2wceq 1455 . . 3  wff  ran  F  =  B
85, 7wa 375 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 189 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  5812  foeq2  5813  foeq3  5814  nffo  5815  fof  5816  forn  5819  dffo2  5820  dffn4  5822  fores  5825  dff1o2  5842  dff1o3  5843  foimacnv  5854  foun  5855  fconst5  6146  fconstfvOLD  6152  dff1o6  6199  nvof1o  6204  f1oweALT  6804  fo1st  6840  fo2nd  6841  tposfo2  7022  fodomr  7749  f1finf1o  7824  unfilem2  7862  brwdom2  8114  harwdom  8131  infpwfien  8519  alephiso  8555  brdom3  8982  brdom5  8983  brdom4  8984  iunfo  8990  qnnen  14315  isfull2  15865  odf1o2  17271  cygctb  17575  qtopss  20779  qtopomap  20782  qtopcmap  20783  reeff1o  23451  efifo  23545  fargshiftfo  25415  pjfoi  27405  ghomfo  30358  bdayfo  30613  fobigcup  30716
  Copyright terms: Public domain W3C validator