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

Definition df-f1o 4674
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5401, dff1o3 5402, dff1o4 5404, and dff1o5 5405. 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 4658 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4656 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4657 . . 3  wff  F : A -onto-> B
75, 6wa 360 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 178 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  5387  f1oeq2  5388  f1oeq3  5389  nff1o  5394  f1of1  5395  dff1o2  5401  dff1o5  5405  f1oco  5420  fo00  5433  dff1o6  5711  fcof1o  5723  soisoi  5745  f1oweALT  5771  tposf1o2  6180  smoiso2  6340  f1finf1o  7040  unfilem2  7076  fofinf1o  7091  alephiso  7679  cnref1o  10302  1arith  12922  xpsff1o  13418  isffth2  13738  ffthf1o  13741  orbsta  14715  odf1o1  14831  znf1o  16453  cygznlem3  16471  reeff1o  19771  recosf1o  19845  efif1olem4  19855  dvdsmulf1o  20382  unopf1o  22442  nvof1o  22983  ghomf1olem  23359  dff1o6f  24444  trnij  24968
  Copyright terms: Public domain W3C validator