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 | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | ⊢ 𝐹 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | cB | ⊢ 𝐵 | |
| 3 | 1 2 0 | wf1 | ⊢ 𝐹 : 𝐴 –1-1→ 𝐵 |
| 4 | 1 2 0 | wf | ⊢ 𝐹 : 𝐴 ⟶ 𝐵 |
| 5 | 0 | ccnv | ⊢ ◡ 𝐹 |
| 6 | 5 | wfun | ⊢ Fun ◡ 𝐹 |
| 7 | 4 6 | wa | ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) |
| 8 | 3 7 | wb | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ) |