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

Definition df-f1o 5447
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5665, dff1o3 5666, dff1o4 5668, and dff1o5 5669. 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 5439 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5437 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5438 . . 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  5651  f1oeq2  5652  f1oeq3  5653  nff1o  5658  f1of1  5659  dff1o2  5665  dff1o5  5669  f1oco  5684  fo00  5697  dff1o6  5999  fcof1o  6012  soisoi  6034  f1oweALT  6060  tposf1o2  6491  smoiso2  6617  f1finf1o  7321  unfilem2  7358  fofinf1o  7373  alephiso  7963  cnref1o  10591  1arith  13278  xpsff1o  13776  isffth2  14096  ffthf1o  14099  orbsta  15073  odf1o1  15189  znf1o  16815  cygznlem3  16833  reeff1o  20346  recosf1o  20420  efif1olem4  20430  dvdsmulf1o  20962  eupatrl  21673  unopf1o  23402  nvof1o  24023  ghomf1olem  25088  frgrancvvdeqlem8  28185
  Copyright terms: Public domain W3C validator