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

Definition df-f1o 5503
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5729, dff1o3 5730, dff1o4 5732, and dff1o5 5733. 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 5495 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5493 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5494 . . 3  wff  F : A -onto-> B
75, 6wa 367 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 184 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  5715  f1oeq2  5716  f1oeq3  5717  nff1o  5722  f1of1  5723  dff1o2  5729  dff1o5  5733  f1oco  5746  fo00  5757  dff1o6  6082  nvof1o  6087  fcof1od  6098  soisoi  6125  f1oweALT  6683  tposf1o2  6899  smoiso2  6958  f1finf1o  7662  unfilem2  7700  fofinf1o  7716  alephiso  8392  cnref1o  11134  wwlktovf1o  12808  1arith  14447  xpsff1o  14975  isffth2  15322  ffthf1o  15325  orbsta  16468  symgextf1o  16565  symgfixf1o  16582  odf1o1  16709  znf1o  18681  cygznlem3  18699  scmatf1o  19119  m2cpmf1o  19343  pm2mpf1o  19401  reeff1o  22927  recosf1o  23007  efif1olem4  23017  dvdsmulf1o  23587  wlknwwlknbij  24834  wlkiswwlkbij  24841  wwlkextbij0  24853  clwwlkf1o  24919  clwlkf1oclwwlk  24972  eupatrl  25089  frgrancvvdeqlem8  25161  numclwlk1lem2f1o  25217  unopf1o  26951  ghomf1olem  29223  sumnnodd  31802  dvnprodlem1  31909  fourierdlem54  32109
  Copyright terms: Public domain W3C validator