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

Definition df-fo 5277
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 5471, dffo3 5691, dffo4 5692, and dffo5 5693. (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 5269 . 2  wff  F : A -onto-> B
53, 1wfn 5266 . . 3  wff  F  Fn  A
63crn 4706 . . . 4  class  ran  F
76, 2wceq 1632 . . 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  5463  foeq2  5464  foeq3  5465  nffo  5466  fof  5467  forn  5470  dffo2  5471  dffn4  5473  fores  5476  dff1o2  5493  dff1o3  5494  foimacnv  5506  foun  5507  fconst5  5747  fconstfv  5750  dff1o6  5807  f1oweALT  5867  fo1st  6155  fo2nd  6156  tposfo2  6273  fodomr  7028  f1finf1o  7102  unfilem2  7138  brwdom2  7303  harwdom  7320  infpwfien  7705  alephiso  7741  brdom3  8169  brdom5  8170  brdom4  8171  iunfo  8177  qnnen  12508  isfull2  13801  odf1o2  14900  cygctb  15194  qtopss  17422  qtopomap  17425  qtopcmap  17426  reeff1o  19839  efifo  19925  pjfoi  22298  nvof1o  23052  ghomfo  24013  bdayfo  24400  fobigcup  24511  dff1o6f  25195  trnij  25718  fargshiftfo  28383
  Copyright terms: Public domain W3C validator