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 6568
and dff13 7004. 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 17337. (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 6346 | . 2 wff 𝐹:𝐴–1-1→𝐵 |
5 | 1, 2, 3 | wf 6345 | . . 3 wff 𝐹:𝐴⟶𝐵 |
6 | 3 | ccnv 5548 | . . . 4 class ◡𝐹 |
7 | 6 | wfun 6343 | . . 3 wff Fun ◡𝐹 |
8 | 5, 7 | wa 396 | . 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) |
9 | 4, 8 | wb 207 | 1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
This definition is referenced by: f1eq1 6564 f1eq2 6565 f1eq3 6566 nff1 6567 dff12 6568 f1f 6569 f1ss 6574 f1ssr 6575 f1ssres 6576 f1cnvcnv 6578 f1co 6579 dff1o2 6614 f1f1orn 6620 f1imacnv 6625 f10 6641 fpropnf1 7016 nvof1o 7028 f1iunw 7633 f1iun 7636 f11o 7639 f1o2ndf1 7809 tz7.48lem 8068 ssdomg 8544 domunsncan 8606 sbthlem9 8624 fodomr 8657 1sdom 8710 fsuppcolem 8853 fsuppco 8854 enfin1ai 9795 injresinj 13148 cshinj 14163 isercolllem2 15012 isercoll 15014 ismon2 16994 isepi2 17001 isfth2 17175 fthoppc 17183 odf1o2 18629 frlmlbs 20871 f1lindf 20896 usgrislfuspgr 26897 subusgr 26999 trlf1 27408 trlres 27410 upgrf1istrl 27413 pthdivtx 27438 spthdifv 27442 spthdep 27443 upgrwlkdvdelem 27445 upgrwlkdvde 27446 spthonepeq 27461 usgr2pth 27473 pthdlem1 27475 uspgrn2crct 27514 crctcshtrl 27529 rinvf1o 30304 swrdrndisj 30559 cycpmfvlem 30682 cycpmfv1 30683 cycpmfv2 30684 cycpmfv3 30685 cycpmcl 30686 madjusmdetlem4 30995 omssubadd 31458 pthhashvtx 32272 subfacp1lem3 32327 subfacp1lem5 32329 diophrw 39236 |
Copyright terms: Public domain | W3C validator |