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

Definition df-fo 4652
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 5358, dffo3 5574, dffo4 5575, and dffo5 5576. (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 4636 . 2  wff  F : A -onto-> B
53, 1wfn 4633 . . 3  wff  F  Fn  A
63crn 4627 . . . 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  5350  foeq2  5351  foeq3  5352  nffo  5353  fof  5354  forn  5357  dffo2  5358  dffn4  5360  fores  5363  dff1o2  5380  dff1o3  5381  foimacnv  5393  foun  5394  fconst5  5630  fconstfv  5633  dff1o6  5690  f1oweALT  5750  fo1st  6038  fo2nd  6039  tposfo2  6156  fodomr  6945  f1finf1o  7019  unfilem2  7055  brwdom2  7220  harwdom  7237  infpwfien  7622  alephiso  7658  brdom3  8086  brdom5  8087  brdom4  8088  iunfo  8094  qnnen  12419  isfull2  13712  odf1o2  14811  cygctb  15105  qtopss  17333  qtopomap  17336  qtopcmap  17337  reeff1o  19750  efifo  19836  pjfoi  22225  nvof1o  22962  ghomfo  23335  axbday  23662  fobigcup  23781  dff1o6f  24423  trnij  24947
  Copyright terms: Public domain W3C validator