Theorem f1oi 6856

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 6661	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6565	. . . 4 ⊢ Fun I
3		cnvi 5865	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6554	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6610	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6071	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6823	. 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 5549  ^◡ccnv 5654  ran crn 5656   ↾ cres 5657  Fun wfun 6527   Fn wfn 6528  –1-1-onto→wf1o 6532

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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1ovi  6858  fveqf1o  7303  f1ofvswap  7307  isoid  7330  enrefg  8990  ssdomg  9006  enreffi  9177  ssdomfi  9190  ssdomfi2  9191  wdomref  9544  infxpenc  10021  pwfseqlem5  10672  fproddvdsd  16425  wunndx  17287  idfucl  17970  idffth  18024  ressffth  18029  setccatid  18173  estrccatid  18220  funcestrcsetclem7  18234  funcestrcsetclem8  18235  equivestrcsetc  18240  funcsetcestrclem7  18249  funcsetcestrclem8  18250  idmgmhm  18803  idmhm  18903  ielefmnd  18996  sursubmefmnd  19005  injsubmefmnd  19006  idghm  19358  idresperm  19513  ricref  20659  islinds2  22026  lindfres  22036  lindsmm  22041  mdetunilem9  22842  ssidcn  23480  resthauslem  23588  sshauslem  23597  idqtop  23932  fmid  24186  iducn  24508  mbfid  25863  dvid  26145  dvexp  26180  wilthlem2  27305  wilthlem3  27306  idmot  28879  ausgrusgrb  29625  upgrres1  29773  umgrres1  29774  usgrres1  29775  usgrexilem  29900  sizusglecusglem1  29921  pliguhgr  30967  hoif  32235  idunop  32459  idcnop  32462  elunop2  32494  fcobijfs  33192  fcobijfs2  33193  symgcom  33523  fzo0pmtrlast  33532  pmtridf1o  33534  cycpmfvlem  33552  cycpmfv3  33555  cycpmcl  33556  islinds5  33802  ellspds  33803  qqhre  34530  rrhre  34531  subfacp1lem4  35762  subfacp1lem5  35763  poimirlem15  38384  poimirlem22  38391  idlaut  40969  tendoidcl  41642  tendo0co2  41661  erng1r  41868  dvalveclem  41898  dva0g  41900  dvh0g  41984  mzpresrename  43595  eldioph2lem1  43605  eldioph2lem2  43606  diophren  43654  kelac2  43906  lnrfg  43960  fundcmpsurbijinjpreimafv  48307  fundcmpsurinjimaid  48311  grimidvtxedg  48801  ushggricedg  48843  stgrusgra  48875  grlicref  48928  gpgusgra  48973  gpg5grlim  49009  uspgrsprfo  49064  funcringcsetcALTV2lem8  49212  funcringcsetclem8ALTV  49235  itcovalendof  49599  tposidf1o  49813  idfu1stf1o  50025  imaidfu  50036  idfth  50084  idsubc  50086  fucoppc  50336  oduoppcciso  50492