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

Definition df-f1o 4302
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5000, dff1o3 5001, dff1o4 5003, and dff1o5 5004. 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 4286 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4284 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4285 . . 3  wff  F : A -onto-> B
75, 6wa 357 . 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  4989  f1oeq2  4990  f1oeq3  4991  hbf1o  4993  f1of1  4994  dff1o2  5000  dff1o5  5004  f1oco  5018  fo00  5031  dff1o6  5296  fcof1o  5310  soisoi  5323  f1oweALT  5347  tposf1o2  5735  smoiso2  5833  f1finf1o  6554  unfilem2  6585  fofinf1o  6600  alephiso  7187  cnref1o  9422  1arith  11429  xpsff1o  11898  orbsta  12671  znf1o  14178  odf1o1  14364  reeff1o  17426  recosf1o  17494  efif1olem4  17503  dvdsmulf1o  17895  unopf1o  19717  ghomf1olem  20581  dff1o6f  21633  trnij  22166
Copyright terms: Public domain