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

Definition df-f1o 5608
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5836, dff1o3 5837, dff1o4 5839, and dff1o5 5840. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1o  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf1o 5600 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5598 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5599 . . 3  wff  F : A -onto-> B
75, 6wa 370 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 187 1  wff  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
Colors of variables: wff setvar class
This definition is referenced by:  f1oeq1  5822  f1oeq2  5823  f1oeq3  5824  nff1o  5829  f1of1  5830  dff1o2  5836  dff1o5  5840  f1oco  5853  fo00  5864  dff1o6  6189  nvof1o  6194  fcof1od  6207  soisoi  6234  f1oweALT  6791  tposf1o2  7007  smoiso2  7096  f1finf1o  7804  unfilem2  7842  fofinf1o  7858  alephiso  8527  cnref1o  11297  wwlktovf1o  13013  1arith  14834  xpsff1o  15425  isffth2  15772  ffthf1o  15775  orbsta  16918  symgextf1o  17015  symgfixf1o  17032  odf1o1  17159  znf1o  19053  cygznlem3  19071  scmatf1o  19488  m2cpmf1o  19712  pm2mpf1o  19770  reeff1o  23267  recosf1o  23349  efif1olem4  23359  dvdsmulf1o  23986  wlknwwlknbij  25286  wlkiswwlkbij  25293  wwlkextbij0  25305  clwwlkf1o  25371  clwlkf1oclwwlk  25424  eupatrl  25541  frgrancvvdeqlem8  25613  numclwlk1lem2f1o  25669  unopf1o  27404  ghomf1olem  30100  poimirlem26  31670  poimirlem27  31671  wessf1ornlem  37082  sumnnodd  37282  dvnprodlem1  37390  fourierdlem54  37592
  Copyright terms: Public domain W3C validator