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

Definition df-f1o 5453
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5671, dff1o3 5672, dff1o4 5674, and dff1o5 5675. 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 5445 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5443 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5444 . . 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  5657  f1oeq2  5658  f1oeq3  5659  nff1o  5664  f1of1  5665  dff1o2  5671  dff1o5  5675  f1oco  5690  fo00  5703  dff1o6  6005  fcof1o  6018  soisoi  6040  f1oweALT  6066  tposf1o2  6497  smoiso2  6623  f1finf1o  7327  unfilem2  7364  fofinf1o  7379  alephiso  7971  cnref1o  10599  1arith  13287  xpsff1o  13785  isffth2  14105  ffthf1o  14108  orbsta  15082  odf1o1  15198  znf1o  16824  cygznlem3  16842  reeff1o  20355  recosf1o  20429  efif1olem4  20439  dvdsmulf1o  20971  eupatrl  21682  unopf1o  23411  nvof1o  24032  ghomf1olem  25097  frgrancvvdeqlem8  28366
  Copyright terms: Public domain W3C validator