![]() |
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 6138
and dff13 6552. 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 16784. (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 5923 | . 2 wff 𝐹:𝐴–1-1→𝐵 |
5 | 1, 2, 3 | wf 5922 | . . 3 wff 𝐹:𝐴⟶𝐵 |
6 | 3 | ccnv 5142 | . . . 4 class ◡𝐹 |
7 | 6 | wfun 5920 | . . 3 wff Fun ◡𝐹 |
8 | 5, 7 | wa 383 | . 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) |
9 | 4, 8 | wb 196 | 1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
This definition is referenced by: f1eq1 6134 f1eq2 6135 f1eq3 6136 nff1 6137 dff12 6138 f1f 6139 f1ss 6144 f1ssr 6145 f1ssres 6146 f1cnvcnv 6147 f1co 6148 dff1o2 6180 f1f1orn 6186 f1imacnv 6191 f10 6207 fpropnf1 6564 nvof1o 6576 fun11iun 7168 f11o 7170 f1o2ndf1 7330 tz7.48lem 7581 ssdomg 8043 domunsncan 8101 sbthlem9 8119 fodomr 8152 1sdom 8204 fsuppcolem 8347 fsuppco 8348 enfin1ai 9244 injresinj 12629 cshinj 13603 isercolllem2 14440 isercoll 14442 ismon2 16441 isepi2 16448 isfth2 16622 fthoppc 16630 odf1o2 18034 frlmlbs 20184 f1lindf 20209 usgrislfuspgr 26124 subusgr 26226 trlf1 26651 trlres 26653 upgrf1istrl 26656 pthdivtx 26681 spthdifv 26685 spthdep 26686 upgrwlkdvdelem 26688 upgrwlkdvde 26689 spthonepeq 26704 usgr2pth 26716 pthdlem1 26718 uspgrn2crct 26756 crctcshtrl 26771 rinvf1o 29560 madjusmdetlem4 30024 omssubadd 30490 subfacp1lem3 31290 subfacp1lem5 31292 diophrw 37639 |
Copyright terms: Public domain | W3C validator |