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

Definition df-fo 5261
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 5455, dffo3 5675, dffo4 5676, and dffo5 5677. (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 5253 . 2  wff  F : A -onto-> B
53, 1wfn 5250 . . 3  wff  F  Fn  A
63crn 4690 . . . 4  class  ran  F
76, 2wceq 1623 . . 3  wff  ran  F  =  B
85, 7wa 358 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 176 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5447  foeq2  5448  foeq3  5449  nffo  5450  fof  5451  forn  5454  dffo2  5455  dffn4  5457  fores  5460  dff1o2  5477  dff1o3  5478  foimacnv  5490  foun  5491  fconst5  5731  fconstfv  5734  dff1o6  5791  f1oweALT  5851  fo1st  6139  fo2nd  6140  tposfo2  6257  fodomr  7012  f1finf1o  7086  unfilem2  7122  brwdom2  7287  harwdom  7304  infpwfien  7689  alephiso  7725  brdom3  8153  brdom5  8154  brdom4  8155  iunfo  8161  qnnen  12492  isfull2  13785  odf1o2  14884  cygctb  15178  qtopss  17406  qtopomap  17409  qtopcmap  17410  reeff1o  19823  efifo  19909  pjfoi  22282  nvof1o  23036  ghomfo  23998  bdayfo  24329  fobigcup  24440  dff1o6f  25092  trnij  25615
  Copyright terms: Public domain W3C validator