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

Definition df-fo 4687
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 5393, dffo3 5609, dffo4 5610, and dffo5 5611. (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 4671 . 2  wff  F : A -onto-> B
53, 1wfn 4668 . . 3  wff  F  Fn  A
63crn 4662 . . . 4  class  ran  F
76, 2wceq 1619 . . 3  wff  ran  F  =  B
85, 7wa 360 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 178 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5385  foeq2  5386  foeq3  5387  nffo  5388  fof  5389  forn  5392  dffo2  5393  dffn4  5395  fores  5398  dff1o2  5415  dff1o3  5416  foimacnv  5428  foun  5429  fconst5  5665  fconstfv  5668  dff1o6  5725  f1oweALT  5785  fo1st  6073  fo2nd  6074  tposfo2  6191  fodomr  6980  f1finf1o  7054  unfilem2  7090  brwdom2  7255  harwdom  7272  infpwfien  7657  alephiso  7693  brdom3  8121  brdom5  8122  brdom4  8123  iunfo  8129  qnnen  12454  isfull2  13747  odf1o2  14846  cygctb  15140  qtopss  17368  qtopomap  17371  qtopcmap  17372  reeff1o  19785  efifo  19871  pjfoi  22242  nvof1o  22997  ghomfo  23370  axbday  23697  fobigcup  23816  dff1o6f  24458  trnij  24982
  Copyright terms: Public domain W3C validator