ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-f1o Unicode version

Definition df-f1o 5225
Description: Define a one-to-one onto function. 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 5217 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5215 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5216 . . 3  wff  F : A -onto-> B
75, 6wa 104 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 105 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  5451  f1oeq2  5452  f1oeq3  5453  nff1o  5461  f1of1  5462  dff1o2  5468  dff1o5  5472  f1oco  5486  fo00  5499  dff1o6  5779  fcof1o  5792  tposf1o2  6273  cnref1o  9652  1arith  12367  xpsff1o  12773  reeff1o  14233  ioocosf1o  14314
  Copyright terms: Public domain W3C validator