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

Definition df-fo 5452
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 5649, dffo3 5876, dffo4 5877, and dffo5 5878. (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 5444 . 2  wff  F : A -onto-> B
53, 1wfn 5441 . . 3  wff  F  Fn  A
63crn 4871 . . . 4  class  ran  F
76, 2wceq 1652 . . 3  wff  ran  F  =  B
85, 7wa 359 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 177 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5641  foeq2  5642  foeq3  5643  nffo  5644  fof  5645  forn  5648  dffo2  5649  dffn4  5651  fores  5654  dff1o2  5671  dff1o3  5672  foimacnv  5684  foun  5685  fconst5  5941  fconstfv  5946  dff1o6  6005  f1oweALT  6066  fo1st  6358  fo2nd  6359  tposfo2  6494  fodomr  7250  f1finf1o  7327  unfilem2  7364  brwdom2  7533  harwdom  7550  infpwfien  7935  alephiso  7971  brdom3  8398  brdom5  8399  brdom4  8400  iunfo  8406  qnnen  12805  isfull2  14100  odf1o2  15199  cygctb  15493  qtopss  17739  qtopomap  17742  qtopcmap  17743  reeff1o  20355  efifo  20441  fargshiftfo  21617  pjfoi  23197  nvof1o  24032  ghomfo  25094  bdayfo  25622  fobigcup  25737
  Copyright terms: Public domain W3C validator