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

Definition df-f1o 4289
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5008, dff1o3 5009, dff1o4 5011, and dff1o5 5012. 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 4273 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4271 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4272 . . 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  4997  f1oeq2  4998  f1oeq3  4999  hbf1o  5001  f1of1  5002  dff1o2  5008  dff1o5  5012  f1oco  5026  fo00  5039  dff1o6  5308  fcof1o  5322  soisoi  5335  f1oweALT  5359  tposf1o2  5749  smoiso2  5847  f1finf1o  6575  unfilem2  6611  fofinf1o  6626  alephiso  7213  cnref1o  9733  1arith  12095  xpsff1o  12571  orbsta  13493  odf1o1  13609  znf1o  15229  cygznlem3  15246  reeff1o  18428  recosf1o  18498  efif1olem4  18507  dvdsmulf1o  19005  unopf1o  21048  ghomf1olem  21894  dff1o6f  22924  trnij  23455
Copyright terms: Public domain