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

Definition df-f1o 4607
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5334, dff1o3 5335, dff1o4 5337, and dff1o5 5338. 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 4591 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4589 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4590 . . 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  5320  f1oeq2  5321  f1oeq3  5322  nff1o  5327  f1of1  5328  dff1o2  5334  dff1o5  5338  f1oco  5353  fo00  5366  dff1o6  5643  fcof1o  5655  soisoi  5677  f1oweALT  5703  tposf1o2  6112  smoiso2  6272  f1finf1o  6971  unfilem2  7007  fofinf1o  7022  alephiso  7609  cnref1o  10228  1arith  12848  xpsff1o  13344  isffth2  13634  ffthf1o  13637  orbsta  14602  odf1o1  14718  znf1o  16337  cygznlem3  16355  reeff1o  19655  recosf1o  19729  efif1olem4  19739  dvdsmulf1o  20266  unopf1o  22326  ghomf1olem  23172  dff1o6f  24257  trnij  24781
  Copyright terms: Public domain W3C validator