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

Definition df-fo 5584
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 5789, dffo3 6031, dffo4 6032, and dffo5 6033. (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 5576 . 2  wff  F : A -onto-> B
53, 1wfn 5573 . . 3  wff  F  Fn  A
63crn 4990 . . . 4  class  ran  F
76, 2wceq 1383 . . 3  wff  ran  F  =  B
85, 7wa 369 . 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  5781  foeq2  5782  foeq3  5783  nffo  5784  fof  5785  forn  5788  dffo2  5789  dffn4  5791  fores  5794  dff1o2  5811  dff1o3  5812  foimacnv  5823  foun  5824  fconst5  6113  fconstfvOLD  6119  dff1o6  6166  nvof1o  6171  f1oweALT  6769  fo1st  6805  fo2nd  6806  tposfo2  6980  fodomr  7670  f1finf1o  7748  unfilem2  7787  brwdom2  8002  harwdom  8019  infpwfien  8446  alephiso  8482  brdom3  8909  brdom5  8910  brdom4  8911  iunfo  8917  qnnen  13929  isfull2  15259  odf1o2  16572  cygctb  16873  qtopss  20194  qtopomap  20197  qtopcmap  20198  reeff1o  22820  efifo  22912  fargshiftfo  24616  pjfoi  26599  ghomfo  29009  bdayfo  29411  fobigcup  29526
  Copyright terms: Public domain W3C validator