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

Definition df-f1o 5228
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5442, dff1o3 5443, dff1o4 5445, and dff1o5 5446. 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 5220 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5218 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5219 . . 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  5428  f1oeq2  5429  f1oeq3  5430  nff1o  5435  f1of1  5436  dff1o2  5442  dff1o5  5446  f1oco  5461  fo00  5474  dff1o6  5752  fcof1o  5764  soisoi  5786  f1oweALT  5812  tposf1o2  6221  smoiso2  6381  f1finf1o  7081  unfilem2  7117  fofinf1o  7132  alephiso  7720  cnref1o  10344  1arith  12968  xpsff1o  13464  isffth2  13784  ffthf1o  13787  orbsta  14761  odf1o1  14877  znf1o  16499  cygznlem3  16517  reeff1o  19817  recosf1o  19891  efif1olem4  19901  dvdsmulf1o  20428  unopf1o  22488  nvof1o  23029  ghomf1olem  23405  dff1o6f  24490  trnij  25014
  Copyright terms: Public domain W3C validator