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

Definition df-f1o 5461
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5679, dff1o3 5680, dff1o4 5682, and dff1o5 5683. 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 5453 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5451 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5452 . . 3  wff  F : A -onto-> B
75, 6wa 359 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 177 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  5665  f1oeq2  5666  f1oeq3  5667  nff1o  5672  f1of1  5673  dff1o2  5679  dff1o5  5683  f1oco  5698  fo00  5711  dff1o6  6013  fcof1o  6026  soisoi  6048  f1oweALT  6074  tposf1o2  6505  smoiso2  6631  f1finf1o  7335  unfilem2  7372  fofinf1o  7387  alephiso  7979  cnref1o  10607  1arith  13295  xpsff1o  13793  isffth2  14113  ffthf1o  14116  orbsta  15090  odf1o1  15206  znf1o  16832  cygznlem3  16850  reeff1o  20363  recosf1o  20437  efif1olem4  20447  dvdsmulf1o  20979  eupatrl  21690  unopf1o  23419  nvof1o  24040  ghomf1olem  25105  frgrancvvdeqlem8  28429
  Copyright terms: Public domain W3C validator