HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-f1o 4279
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4996, dff1o3 4997, dff1o4 4999, and dff1o5 5000. 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 4263 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4261 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4262 . . 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  4985  f1oeq2  4986  f1oeq3  4987  hbf1o  4989  f1of1  4990  dff1o2  4996  dff1o5  5000  f1oco  5014  fo00  5027  dff1o6  5295  fcof1o  5309  soisoi  5322  f1oweALT  5346  tposf1o2  5735  smoiso2  5833  f1finf1o  6559  unfilem2  6595  fofinf1o  6610  alephiso  7197  cnref1o  9432  1arith  11457  xpsff1o  11932  orbsta  12775  znf1o  14269  odf1o1  14455  reeff1o  17517  recosf1o  17585  efif1olem4  17594  dvdsmulf1o  17986  unopf1o  19812  ghomf1olem  20670  dff1o6f  21709  trnij  22241
Copyright terms: Public domain