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

Definition df-f1o 4604
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5331, dff1o3 5332, dff1o4 5334, and dff1o5 5335. 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 4588 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4586 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4587 . . 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  5317  f1oeq2  5318  f1oeq3  5319  nff1o  5324  f1of1  5325  dff1o2  5331  dff1o5  5335  f1oco  5350  fo00  5363  dff1o6  5640  fcof1o  5652  soisoi  5674  f1oweALT  5700  tposf1o2  6109  smoiso2  6269  f1finf1o  6968  unfilem2  7004  fofinf1o  7019  alephiso  7606  cnref1o  10195  1arith  12810  xpsff1o  13306  isffth2  13596  ffthf1o  13599  orbsta  14564  odf1o1  14680  znf1o  16299  cygznlem3  16317  reeff1o  19617  recosf1o  19687  efif1olem4  19696  dvdsmulf1o  20200  unopf1o  22257  ghomf1olem  23103  dff1o6f  24188  trnij  24712
  Copyright terms: Public domain W3C validator