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 6102
Description: Define a one-to-one function. For equivalent definitions see dff12 6311 and dff13 6732. 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 16937. (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 6094 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 6093 . . 3 wff 𝐹:𝐴𝐵
63ccnv 5310 . . . 4 class 𝐹
76wfun 6091 . . 3 wff Fun 𝐹
85, 7wa 384 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 197 1 wff (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
This definition is referenced by:  f1eq1  6307  f1eq2  6308  f1eq3  6309  nff1  6310  dff12  6311  f1f  6312  f1ss  6317  f1ssr  6318  f1ssres  6319  f1cnvcnv  6321  f1co  6322  dff1o2  6354  f1f1orn  6360  f1imacnv  6365  f10  6381  fpropnf1  6744  nvof1o  6756  fun11iun  7352  f11o  7354  f1o2ndf1  7515  tz7.48lem  7768  ssdomg  8234  domunsncan  8295  sbthlem9  8313  fodomr  8346  1sdom  8398  fsuppcolem  8541  fsuppco  8542  enfin1ai  9487  injresinj  12809  cshinj  13777  isercolllem2  14615  isercoll  14617  ismon2  16594  isepi2  16601  isfth2  16775  fthoppc  16783  odf1o2  18185  frlmlbs  20342  f1lindf  20367  usgrislfuspgr  26290  subusgr  26393  trlf1  26819  trlres  26821  upgrf1istrl  26824  pthdivtx  26849  spthdifv  26853  spthdep  26854  upgrwlkdvdelem  26856  upgrwlkdvde  26857  spthonepeq  26872  usgr2pth  26884  pthdlem1  26886  uspgrn2crct  26925  crctcshtrl  26940  rinvf1o  29755  madjusmdetlem4  30217  omssubadd  30683  subfacp1lem3  31482  subfacp1lem5  31484  diophrw  37818
  Copyright terms: Public domain W3C validator