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

Definition df-fo 4606
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 5312, dffo3 5527, dffo4 5528, and dffo5 5529. (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 4590 . 2  wff  F : A -onto-> B
53, 1wfn 4587 . . 3  wff  F  Fn  A
63crn 4581 . . . 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  5304  foeq2  5305  foeq3  5306  nffo  5307  fof  5308  forn  5311  dffo2  5312  dffn4  5314  fores  5317  dff1o2  5334  dff1o3  5335  foimacnv  5347  foun  5348  fconst5  5583  fconstfv  5586  dff1o6  5643  f1oweALT  5703  fo1st  5991  fo2nd  5992  tposfo2  6109  fodomr  6897  f1finf1o  6971  unfilem2  7007  brwdom2  7171  harwdom  7188  infpwfien  7573  alephiso  7609  brdom3  8037  brdom5  8038  brdom4  8039  iunfo  8045  qnnen  12366  isfull2  13629  odf1o2  14719  cygctb  15013  qtopss  17238  qtopomap  17241  qtopcmap  17242  reeff1o  19655  efifo  19741  pjfoi  22130  ghomfo  23169  axbday  23496  fobigcup  23615  dff1o6f  24257  trnij  24781
  Copyright terms: Public domain W3C validator