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

Definition df-fo 5423
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 5620, dffo3 5847, dffo4 5848, and dffo5 5849. (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 5415 . 2  wff  F : A -onto-> B
53, 1wfn 5412 . . 3  wff  F  Fn  A
63crn 4842 . . . 4  class  ran  F
76, 2wceq 1649 . . 3  wff  ran  F  =  B
85, 7wa 359 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 177 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5612  foeq2  5613  foeq3  5614  nffo  5615  fof  5616  forn  5619  dffo2  5620  dffn4  5622  fores  5625  dff1o2  5642  dff1o3  5643  foimacnv  5655  foun  5656  fconst5  5912  fconstfv  5917  dff1o6  5976  f1oweALT  6037  fo1st  6329  fo2nd  6330  tposfo2  6465  fodomr  7221  f1finf1o  7298  unfilem2  7335  brwdom2  7501  harwdom  7518  infpwfien  7903  alephiso  7939  brdom3  8366  brdom5  8367  brdom4  8368  iunfo  8374  qnnen  12772  isfull2  14067  odf1o2  15166  cygctb  15460  qtopss  17704  qtopomap  17707  qtopcmap  17708  reeff1o  20320  efifo  20406  fargshiftfo  21582  pjfoi  23162  nvof1o  23997  ghomfo  25059  bdayfo  25547  fobigcup  25658
  Copyright terms: Public domain W3C validator