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

Definition df-f1o 4852
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 : -1-1-onto->  F : -1-1->  F : -onto->

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3  F
41, 2, 3wf1o 4844 . 2  F :
-1-1-onto->
51, 2, 3wf1 4842 . . 3  F : -1-1->
61, 2, 3wfo 4843 . . 3  F : -onto->
75, 6wa 97 . 2  F : -1-1->  F : -onto->
84, 7wb 98 1  F : -1-1-onto->  F : -1-1->  F : -onto->
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5060  f1oeq2  5061  f1oeq3  5062  nff1o  5067  f1of1  5068  dff1o2  5074  dff1o5  5078  f1oco  5092  fo00  5105  dff1o6  5359  fcof1o  5372  tposf1o2  5826  cnref1o  8357
  Copyright terms: Public domain W3C validator