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

Definition df-fo 5400
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 5597, dffo3 5823, dffo4 5824, and dffo5 5825. (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 5392 . 2  wff  F : A -onto-> B
53, 1wfn 5389 . . 3  wff  F  Fn  A
63crn 4819 . . . 4  class  ran  F
76, 2wceq 1649 . . 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  5589  foeq2  5590  foeq3  5591  nffo  5592  fof  5593  forn  5596  dffo2  5597  dffn4  5599  fores  5602  dff1o2  5619  dff1o3  5620  foimacnv  5632  foun  5633  fconst5  5888  fconstfv  5893  dff1o6  5952  f1oweALT  6013  fo1st  6305  fo2nd  6306  tposfo2  6438  fodomr  7194  f1finf1o  7271  unfilem2  7308  brwdom2  7474  harwdom  7491  infpwfien  7876  alephiso  7912  brdom3  8339  brdom5  8340  brdom4  8341  iunfo  8347  qnnen  12740  isfull2  14035  odf1o2  15134  cygctb  15428  qtopss  17668  qtopomap  17671  qtopcmap  17672  reeff1o  20230  efifo  20316  fargshiftfo  21473  pjfoi  23053  nvof1o  23883  ghomfo  24881  bdayfo  25353  fobigcup  25464
  Copyright terms: Public domain W3C validator