Description: Define a one-to-one function. For equivalent definitions see dff12 and dff13 . Compare Definition 6.15(5) of TakeutiZaring p. 27. We use their notation ("1-1" above the arrow).
A one-to-one function is also called an "injection" or an "injective function", F : A -1-1-> B can be read as " F is an injection from A into B ". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon . (Contributed by NM, 1-Aug-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-f1 | |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | |- F |
|
| 1 | cA | |- A |
|
| 2 | cB | |- B |
|
| 3 | 1 2 0 | wf1 | |- F : A -1-1-> B |
| 4 | 1 2 0 | wf | |- F : A --> B |
| 5 | 0 | ccnv | |- `' F |
| 6 | 5 | wfun | |- Fun `' F |
| 7 | 4 6 | wa | |- ( F : A --> B /\ Fun `' F ) |
| 8 | 3 7 | wb | |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) ) |