MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f1 Structured version   Visualization version   GIF version

Definition df-f1 6354
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.)

Assertion
Ref Expression
df-f1 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))

Detailed syntax breakdown of Definition df-f1
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf1 6346 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 6345 . . 3 wff 𝐹:𝐴𝐵
63ccnv 5548 . . . 4 class 𝐹
76wfun 6343 . . 3 wff Fun 𝐹
85, 7wa 396 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 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