Theorem f1oi 6849

Description: A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) Avoid ax-12 2215. (Revised by TM, 10-Feb-2026.)

Assertion

Ref	Expression
f1oi	⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6654	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6557	. . . 4 ⊢ Fun I
3		cnvi 5861	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6546	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6602	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6067	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6816	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1358	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1563   I cid 5545  ^◡ccnv 5650  ran crn 5652   ↾ cres 5653  Fun wfun 6519   Fn wfn 6520  –1-1-onto→wf1o 6524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532

This theorem is referenced by:  f1ovi  6851  fveqf1o  7290  f1ofvswap  7294  isoid  7317  enrefg  8969  ssdomg  8985  enreffi  9155  ssdomfi  9168  ssdomfi2  9169  wdomref  9522  infxpenc  9990  pwfseqlem5  10636  fproddvdsd  16381  wunndx  17243  idfucl  17926  idffth  17980  ressffth  17985  setccatid  18129  estrccatid  18176  funcestrcsetclem7  18190  funcestrcsetclem8  18191  equivestrcsetc  18196  funcsetcestrclem7  18205  funcsetcestrclem8  18206  idmgmhm  18747  idmhm  18841  ielefmnd  18934  sursubmefmnd  18943  injsubmefmnd  18944  idghm  19289  idresperm  19444  islinds2  21920  lindfres  21930  lindsmm  21935  mdetunilem9  22734  ssidcn  23369  resthauslem  23477  sshauslem  23486  idqtop  23820  fmid  24074  iducn  24396  mbfid  25751  dvid  26034  dvexp  26069  wilthlem2  27187  wilthlem3  27188  idmot  28760  ausgrusgrb  29420  upgrres1  29568  umgrres1  29569  usgrres1  29570  usgrexilem  29695  sizusglecusglem1  29716  pliguhgr  30743  hoif  32011  idunop  32235  idcnop  32238  elunop2  32270  fcobijfs  32974  fcobijfs2  32975  symgcom  33311  fzo0pmtrlast  33320  pmtridf1o  33322  cycpmfvlem  33340  cycpmfv3  33343  cycpmcl  33344  islinds5  33592  ellspds  33593  qqhre  34322  rrhre  34323  subfacp1lem4  35541  subfacp1lem5  35542  poimirlem15  38141  poimirlem22  38148  idlaut  40727  tendoidcl  41400  tendo0co2  41419  erng1r  41626  dvalveclem  41656  dva0g  41658  dvh0g  41742  mzpresrename  43338  eldioph2lem1  43348  eldioph2lem2  43349  diophren  43397  kelac2  43649  lnrfg  43703  fundcmpsurbijinjpreimafv  48012  fundcmpsurinjimaid  48016  grimidvtxedg  48506  ushggricedg  48548  stgrusgra  48580  grlicref  48633  gpgusgra  48678  gpg5grlim  48714  uspgrsprfo  48769  funcringcsetcALTV2lem8  48918  funcringcsetclem8ALTV  48941  itcovalendof  49301  tposidf1o  49517  idfu1stf1o  49729  imaidfu  49740  idfth  49788  idsubc  49790  fucoppc  50040  oduoppcciso  50196