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

Definition df-f1o 4281
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4999, dff1o3 5000, dff1o4 5002, and dff1o5 5003. 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 4265 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4263 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4264 . . 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  4988  f1oeq2  4989  f1oeq3  4990  hbf1o  4992  f1of1  4993  dff1o2  4999  dff1o5  5003  f1oco  5017  fo00  5030  dff1o6  5298  fcof1o  5312  soisoi  5325  f1oweALT  5349  tposf1o2  5739  smoiso2  5837  f1finf1o  6565  unfilem2  6601  fofinf1o  6616  alephiso  7203  cnref1o  9443  1arith  11545  xpsff1o  12020  orbsta  12942  odf1o1  13058  znf1o  14675  cygznlem3  14692  reeff1o  17853  recosf1o  17921  efif1olem4  17930  dvdsmulf1o  18380  unopf1o  20319  ghomf1olem  21167  dff1o6f  22199  trnij  22730
Copyright terms: Public domain