| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-f1 | Structured version Visualization version GIF version | ||
| Description: Define a one-to-one
function. For equivalent definitions see dff12 6803
and dff13 7275. 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", 𝐹:𝐴–1-1→𝐵 can be read as "𝐹 is an injection from 𝐴 into 𝐵". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon 18132. (Contributed by NM, 1-Aug-1994.) |
| Ref | Expression |
|---|---|
| df-f1 | ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | cF | . . 3 class 𝐹 | |
| 4 | 1, 2, 3 | wf1 6558 | . 2 wff 𝐹:𝐴–1-1→𝐵 |
| 5 | 1, 2, 3 | wf 6557 | . . 3 wff 𝐹:𝐴⟶𝐵 |
| 6 | 3 | ccnv 5684 | . . . 4 class ◡𝐹 |
| 7 | 6 | wfun 6555 | . . 3 wff Fun ◡𝐹 |
| 8 | 5, 7 | wa 395 | . 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) |
| 9 | 4, 8 | wb 206 | 1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
| Copyright terms: Public domain | W3C validator |