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 6046
Description: Define a one-to-one function. For equivalent definitions see dff12 6253 and dff13 6667. 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 16930. (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 6038 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 6037 . . 3 wff 𝐹:𝐴𝐵
63ccnv 5257 . . . 4 class 𝐹
76wfun 6035 . . 3 wff Fun 𝐹
85, 7wa 383 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 196 1 wff (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
This definition is referenced by:  f1eq1  6249  f1eq2  6250  f1eq3  6251  nff1  6252  dff12  6253  f1f  6254  f1ss  6259  f1ssr  6260  f1ssres  6261  f1cnvcnv  6262  f1co  6263  dff1o2  6295  f1f1orn  6301  f1imacnv  6306  f10  6322  fpropnf1  6679  nvof1o  6691  fun11iun  7283  f11o  7285  f1o2ndf1  7445  tz7.48lem  7697  ssdomg  8159  domunsncan  8217  sbthlem9  8235  fodomr  8268  1sdom  8320  fsuppcolem  8463  fsuppco  8464  enfin1ai  9390  injresinj  12775  cshinj  13749  isercolllem2  14587  isercoll  14589  ismon2  16587  isepi2  16594  isfth2  16768  fthoppc  16776  odf1o2  18180  frlmlbs  20330  f1lindf  20355  usgrislfuspgr  26270  subusgr  26372  trlf1  26797  trlres  26799  upgrf1istrl  26802  pthdivtx  26827  spthdifv  26831  spthdep  26832  upgrwlkdvdelem  26834  upgrwlkdvde  26835  spthonepeq  26850  usgr2pth  26862  pthdlem1  26864  uspgrn2crct  26903  crctcshtrl  26918  rinvf1o  29733  madjusmdetlem4  30197  omssubadd  30663  subfacp1lem3  31463  subfacp1lem5  31465  diophrw  37816
  Copyright terms: Public domain W3C validator