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

Definition df-f1o 5262
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5477, dff1o3 5478, dff1o4 5480, and dff1o5 5481. 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 5254 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5252 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5253 . . 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  5463  f1oeq2  5464  f1oeq3  5465  nff1o  5470  f1of1  5471  dff1o2  5477  dff1o5  5481  f1oco  5496  fo00  5509  dff1o6  5791  fcof1o  5803  soisoi  5825  f1oweALT  5851  tposf1o2  6260  smoiso2  6386  f1finf1o  7086  unfilem2  7122  fofinf1o  7137  alephiso  7725  cnref1o  10349  1arith  12974  xpsff1o  13470  isffth2  13790  ffthf1o  13793  orbsta  14767  odf1o1  14883  znf1o  16505  cygznlem3  16523  reeff1o  19823  recosf1o  19897  efif1olem4  19907  dvdsmulf1o  20434  unopf1o  22496  nvof1o  23036  ghomf1olem  24001  dff1o6f  25092  trnij  25615
  Copyright terms: Public domain W3C validator