MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fo Structured 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 5814, dffo3 6052, dffo4 6053, and dffo5 6054. (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 4855 . . . 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  5806  foeq2  5807  foeq3  5808  nffo  5809  fof  5810  forn  5813  dffo2  5814  dffn4  5816  fores  5819  dff1o2  5836  dff1o3  5837  foimacnv  5848  foun  5849  fconst5  6137  fconstfvOLD  6142  dff1o6  6189  nvof1o  6194  f1oweALT  6791  fo1st  6827  fo2nd  6828  tposfo2  7004  fodomr  7729  f1finf1o  7804  unfilem2  7842  brwdom2  8088  harwdom  8105  infpwfien  8491  alephiso  8527  brdom3  8954  brdom5  8955  brdom4  8956  iunfo  8962  qnnen  14244  isfull2  15767  odf1o2  17160  cygctb  17461  qtopss  20661  qtopomap  20664  qtopcmap  20665  reeff1o  23267  efifo  23361  fargshiftfo  25211  pjfoi  27191  ghomfo  30097  bdayfo  30349  fobigcup  30452
  Copyright terms: Public domain W3C validator