Definition df-f1 5794

Description: Define a one-to-one function. For equivalent definitions see dff12 5997 and dff13 6393. 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 16508. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1 5786	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5785	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5026	. . . 4 class ◡𝐹
7	6	wfun 5783	. . 3 wff Fun ◡𝐹
8	5, 7	wa 382	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 194	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  5993  f1eq2  5994  f1eq3  5995  nff1  5996  dff12  5997  f1f  5998  f1ss  6003  f1ssr  6004  f1ssres  6005  f1cnvcnv  6006  f1co  6007  dff1o2  6039  f1f1orn  6045  f1imacnv  6050  f10  6065  nvof1o  6413  fun11iun  6996  f11o  6998  f1o2ndf1  7149  tz7.48lem  7400  ssdomg  7864  domunsncan  7922  sbthlem9  7940  fodomr  7973  1sdom  8025  fsuppcolem  8166  fsuppco  8167  enfin1ai  9066  injresinj  12408  cshinj  13356  isercolllem2  14192  isercoll  14194  ismon2  16165  isepi2  16172  isfth2  16346  fthoppc  16354  odf1o2  17759  frlmlbs  19902  f1lindf  19927  istrl2  25861  wlkntrllem3  25884  spthonepeq  25910  wlkdvspthlem  25930  wlkdvspth  25931  usgra2wlkspthlem1  25940  usgra2wlkspthlem2  25941  cyclnspth  25952  constr3trllem2  25972  4cycl4dv  25988  usg2wotspth  26204  2spontn0vne  26207  eupatrl  26288  rinvf1o  28607  madjusmdetlem4  29017  omssubadd  29482  subfacp1lem3  30211  subfacp1lem5  30213  diophrw  36123  fpropnf1  40143  usgrislfuspgr  40395  subusgr  40494  trlf1  40887  trlres  40889  upgrf1istrl  40892  pthdivtx  40916  sPthdifv  40920  spthdep  40921  upgrwlkdvdelem  40923  upgrwlkdvde  40924  spthonepeq-av  40939  usgr2pth  40951  pthdlem1  40953  uspgrn2crct  40992  crctcshtrl  41007