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

Definition df-f1o 5278
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5493, dff1o3 5494, dff1o4 5496, and dff1o5 5497. 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 5270 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5268 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5269 . . 3  wff  F : A -onto-> B
75, 6wa 358 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 176 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  5479  f1oeq2  5480  f1oeq3  5481  nff1o  5486  f1of1  5487  dff1o2  5493  dff1o5  5497  f1oco  5512  fo00  5525  dff1o6  5807  fcof1o  5819  soisoi  5841  f1oweALT  5867  tposf1o2  6276  smoiso2  6402  f1finf1o  7102  unfilem2  7138  fofinf1o  7153  alephiso  7741  cnref1o  10365  1arith  12990  xpsff1o  13486  isffth2  13806  ffthf1o  13809  orbsta  14783  odf1o1  14899  znf1o  16521  cygznlem3  16539  reeff1o  19839  recosf1o  19913  efif1olem4  19923  dvdsmulf1o  20450  unopf1o  22512  nvof1o  23052  ghomf1olem  24016  dff1o6f  25194  trnij  25717  eupatrl  28384
  Copyright terms: Public domain W3C validator