Theorem f1oi 6861

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 2213. (Revised by TM, 10-Feb-2026.)

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6666	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6570	. . . 4 ⊢ Fun I
3		cnvi 5863	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6558	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6615	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6073	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6828	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1360	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

This proof depends on syntax axioms:   = wceq 1570   I cid 5545  ^◡ccnv 5650  ran crn 5652   ↾ cres 5653  Fun wfun 6531   Fn wfn 6532  –1-1-onto→wf1o 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  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 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is used by:  f1ovi  6863  fveqf1o  7308  f1ofvswap  7312  isoid  7335  enrefg  9004  ssdomg  9020  enreffi  9191  ssdomfi  9204  ssdomfi2  9205  wdomref  9559  infxpenc  10090  pwfseqlem5  10741  fproddvdsd  16498  wunndx  17366  idfucl  18049  idffth  18103  ressffth  18108  setccatid  18252  estrccatid  18299  funcestrcsetclem7  18313  funcestrcsetclem8  18314  equivestrcsetc  18319  funcsetcestrclem7  18328  funcsetcestrclem8  18329  idmgmhm  18883  idmhm  18983  ielefmnd  19076  sursubmefmnd  19085  injsubmefmnd  19086  idghm  19438  idresperm  19593  ricref  20741  islinds2  22112  lindfres  22122  lindsmm  22127  mdetunilem9  22928  ssidcn  23566  resthauslem  23674  sshauslem  23683  idqtop  24018  fmid  24272  iducn  24594  mbfid  25949  dvid  26231  dvexp  26266  wilthlem2  27389  wilthlem3  27390  idmot  28993  ausgrusgrb  29739  upgrres1  29887  umgrres1  29888  usgrres1  29889  usgrexilem  30014  sizusglecusglem1  30035  pliguhgr  31081  hoif  32349  idunop  32573  idcnop  32576  elunop2  32608  fcobijfs  33306  fcobijfs2  33307  symgcom  33637  fzo0pmtrlast  33646  pmtridf1o  33648  cycpmfvlem  33666  cycpmfv3  33669  cycpmcl  33670  islinds5  33916  ellspds  33917  qqhre  34645  rrhre  34646  subfacp1lem4  35927  subfacp1lem5  35928  poimirlem15  38533  poimirlem22  38540  idlaut  41133  tendoidcl  41806  tendo0co2  41825  erng1r  42032  dvalveclem  42062  dva0g  42064  dvh0g  42148  mzpresrename  43740  eldioph2lem1  43750  eldioph2lem2  43751  diophren  43799  kelac2  44051  lnrfg  44105  fundcmpsurbijinjpreimafv  48458  fundcmpsurinjimaid  48462  grimidvtxedg  48952  ushggricedg  48994  stgrusgra  49026  grlicref  49079  gpgusgra  49124  gpg5grlim  49160  uspgrsprfo  49215  funcringcsetcALTV2lem8  49363  funcringcsetclem8ALTV  49386  itcovalendof  49750  tposidf1o  49964  idfu1stf1o  50176  imaidfu  50187  idfth  50235  idsubc  50237  fucoppc  50487  oduoppcciso  50643