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 5809
Description: Define a one-to-one function. For equivalent definitions see dff12 6013 and dff13 6416. 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 16560. (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 5801 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 5800 . . 3 wff 𝐹:𝐴𝐵
63ccnv 5037 . . . 4 class 𝐹
76wfun 5798 . . 3 wff Fun 𝐹
85, 7wa 383 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 195 1 wff (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
This definition is referenced by:  f1eq1  6009  f1eq2  6010  f1eq3  6011  nff1  6012  dff12  6013  f1f  6014  f1ss  6019  f1ssr  6020  f1ssres  6021  f1cnvcnv  6022  f1co  6023  dff1o2  6055  f1f1orn  6061  f1imacnv  6066  f10  6081  nvof1o  6436  fun11iun  7019  f11o  7021  f1o2ndf1  7172  tz7.48lem  7423  ssdomg  7887  domunsncan  7945  sbthlem9  7963  fodomr  7996  1sdom  8048  fsuppcolem  8189  fsuppco  8190  enfin1ai  9089  injresinj  12451  cshinj  13408  isercolllem2  14244  isercoll  14246  ismon2  16217  isepi2  16224  isfth2  16398  fthoppc  16406  odf1o2  17811  frlmlbs  19955  f1lindf  19980  istrl2  26068  wlkntrllem3  26091  spthonepeq  26117  wlkdvspthlem  26137  wlkdvspth  26138  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  cyclnspth  26159  constr3trllem2  26179  4cycl4dv  26195  usg2wotspth  26411  2spontn0vne  26414  eupatrl  26495  rinvf1o  28814  madjusmdetlem4  29224  omssubadd  29689  subfacp1lem3  30418  subfacp1lem5  30420  diophrw  36340  fpropnf1  40337  usgrislfuspgr  40414  subusgr  40513  trlf1  40906  trlres  40908  upgrf1istrl  40911  pthdivtx  40935  sPthdifv  40939  spthdep  40940  upgrwlkdvdelem  40942  upgrwlkdvde  40943  spthonepeq-av  40958  usgr2pth  40970  pthdlem1  40972  uspgrn2crct  41011  crctcshtrl  41026
  Copyright terms: Public domain W3C validator