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 5862
Description: Define a one-to-one function. For equivalent definitions see dff12 6067 and dff13 6477. 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 16677. (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 5854 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 5853 . . 3 wff 𝐹:𝐴𝐵
63ccnv 5083 . . . 4 class 𝐹
76wfun 5851 . . 3 wff Fun 𝐹
85, 7wa 384 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 196 1 wff (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
This definition is referenced by:  f1eq1  6063  f1eq2  6064  f1eq3  6065  nff1  6066  dff12  6067  f1f  6068  f1ss  6073  f1ssr  6074  f1ssres  6075  f1cnvcnv  6076  f1co  6077  dff1o2  6109  f1f1orn  6115  f1imacnv  6120  f10  6136  fpropnf1  6489  nvof1o  6501  fun11iun  7088  f11o  7090  f1o2ndf1  7245  tz7.48lem  7496  ssdomg  7961  domunsncan  8020  sbthlem9  8038  fodomr  8071  1sdom  8123  fsuppcolem  8266  fsuppco  8267  enfin1ai  9166  injresinj  12545  cshinj  13510  isercolllem2  14346  isercoll  14348  ismon2  16334  isepi2  16341  isfth2  16515  fthoppc  16523  odf1o2  17928  frlmlbs  20076  f1lindf  20101  usgrislfuspgr  26006  subusgr  26108  trlf1  26498  trlres  26500  upgrf1istrl  26503  pthdivtx  26528  spthdifv  26532  spthdep  26533  upgrwlkdvdelem  26535  upgrwlkdvde  26536  spthonepeq  26551  usgr2pth  26563  pthdlem1  26565  uspgrn2crct  26603  crctcshtrl  26618  rinvf1o  29317  madjusmdetlem4  29720  omssubadd  30185  subfacp1lem3  30925  subfacp1lem5  30927  diophrw  36841
  Copyright terms: Public domain W3C validator