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

Definition df-fo 5502
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 5707, dffo3 5948, dffo4 5949, and dffo5 5950. (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 5494 . 2  wff  F : A -onto-> B
53, 1wfn 5491 . . 3  wff  F  Fn  A
63crn 4914 . . . 4  class  ran  F
76, 2wceq 1399 . . 3  wff  ran  F  =  B
85, 7wa 367 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 184 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  5699  foeq2  5700  foeq3  5701  nffo  5702  fof  5703  forn  5706  dffo2  5707  dffn4  5709  fores  5712  dff1o2  5729  dff1o3  5730  foimacnv  5741  foun  5742  fconst5  6031  fconstfvOLD  6035  dff1o6  6082  nvof1o  6087  f1oweALT  6683  fo1st  6719  fo2nd  6720  tposfo2  6896  fodomr  7587  f1finf1o  7662  unfilem2  7700  brwdom2  7914  harwdom  7931  infpwfien  8356  alephiso  8392  brdom3  8819  brdom5  8820  brdom4  8821  iunfo  8827  qnnen  13949  isfull2  15317  odf1o2  16710  cygctb  17011  qtopss  20301  qtopomap  20304  qtopcmap  20305  reeff1o  22927  efifo  23019  fargshiftfo  24759  pjfoi  26738  ghomfo  29220  bdayfo  29600  fobigcup  29703
  Copyright terms: Public domain W3C validator