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

Definition df-f1o 4936
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 4928 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4926 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4927 . . 3  wff  F : A -onto-> B
75, 6wa 101 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 102 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  5144  f1oeq2  5145  f1oeq3  5146  nff1o  5151  f1of1  5152  dff1o2  5158  dff1o5  5162  f1oco  5176  fo00  5189  dff1o6  5443  fcof1o  5456  tposf1o2  5915  cnref1o  8679
  Copyright terms: Public domain W3C validator