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

Definition df-f1o 4586
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5309, dff1o3 5310, dff1o4 5312, and dff1o5 5313. 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 4570 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4568 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4569 . . 3  wff  F : A -onto-> B
75, 6wa 357 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 175 1  wff  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5298  f1oeq2  5299  f1oeq3  5300  nff1o  5302  f1of1  5303  dff1o2  5309  dff1o5  5313  f1oco  5328  fo00  5341  dff1o6  5618  fcof1o  5630  soisoi  5652  f1oweALT  5678  tposf1o2  6086  smoiso2  6246  f1finf1o  6945  unfilem2  6981  fofinf1o  6996  alephiso  7583  cnref1o  10167  1arith  12782  xpsff1o  13278  orbsta  14448  odf1o1  14564  znf1o  16183  cygznlem3  16201  reeff1o  19501  recosf1o  19571  efif1olem4  19580  dvdsmulf1o  20084  unopf1o  22127  ghomf1olem  22973  dff1o6f  24063  trnij  24587
  Copyright terms: Public domain W3C validator