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

Definition df-f1o 4327
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5046, dff1o3 5047, dff1o4 5049, and dff1o5 5050. 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 4311 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4309 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4310 . . 3  wff  F : A -onto-> B
75, 6wa 356 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 174 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  5035  f1oeq2  5036  f1oeq3  5037  hbf1o  5039  f1of1  5040  dff1o2  5046  dff1o5  5050  f1oco  5064  fo00  5077  dff1o6  5346  fcof1o  5360  soisoi  5373  f1oweALT  5397  tposf1o2  5787  smoiso2  5885  f1finf1o  6613  unfilem2  6649  fofinf1o  6664  alephiso  7251  cnref1o  9771  1arith  12133  xpsff1o  12609  orbsta  13531  odf1o1  13647  znf1o  15267  cygznlem3  15284  reeff1o  18466  recosf1o  18536  efif1olem4  18545  dvdsmulf1o  19043  unopf1o  21087  ghomf1olem  21933  dff1o6f  22973  trnij  23505
  Copyright terms: Public domain W3C validator