Theorem f1oi 6863

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6668	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6572	. . . 4 ⊢ Fun I
3		cnvi 5873	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6561	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6617	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6079	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6830	. 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 5557  ^◡ccnv 5662  ran crn 5664   ↾ cres 5665  Fun wfun 6534   Fn wfn 6535  –1-1-onto→wf1o 6539

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1ovi  6865  fveqf1o  7306  f1ofvswap  7310  isoid  7333  enrefg  8983  ssdomg  8999  enreffi  9170  ssdomfi  9183  ssdomfi2  9184  wdomref  9537  infxpenc  10014  pwfseqlem5  10659  fproddvdsd  16410  wunndx  17272  idfucl  17955  idffth  18009  ressffth  18014  setccatid  18158  estrccatid  18205  funcestrcsetclem7  18219  funcestrcsetclem8  18220  equivestrcsetc  18225  funcsetcestrclem7  18234  funcsetcestrclem8  18235  idmgmhm  18780  idmhm  18876  ielefmnd  18969  sursubmefmnd  18978  injsubmefmnd  18979  idghm  19324  idresperm  19479  ricref  20625  islinds2  21992  lindfres  22002  lindsmm  22007  mdetunilem9  22806  ssidcn  23441  resthauslem  23549  sshauslem  23558  idqtop  23892  fmid  24146  iducn  24468  mbfid  25823  dvid  26106  dvexp  26141  wilthlem2  27262  wilthlem3  27263  idmot  28835  ausgrusgrb  29544  upgrres1  29692  umgrres1  29693  usgrres1  29694  usgrexilem  29819  sizusglecusglem1  29840  pliguhgr  30867  hoif  32135  idunop  32359  idcnop  32362  elunop2  32394  fcobijfs  33095  fcobijfs2  33096  symgcom  33426  fzo0pmtrlast  33435  pmtridf1o  33437  cycpmfvlem  33455  cycpmfv3  33458  cycpmcl  33459  islinds5  33705  ellspds  33706  qqhre  34433  rrhre  34434  subfacp1lem4  35688  subfacp1lem5  35689  poimirlem15  38319  poimirlem22  38326  idlaut  40903  tendoidcl  41576  tendo0co2  41595  erng1r  41802  dvalveclem  41832  dva0g  41834  dvh0g  41918  mzpresrename  43514  eldioph2lem1  43524  eldioph2lem2  43525  diophren  43573  kelac2  43825  lnrfg  43879  fundcmpsurbijinjpreimafv  48189  fundcmpsurinjimaid  48193  grimidvtxedg  48683  ushggricedg  48725  stgrusgra  48757  grlicref  48810  gpgusgra  48855  gpg5grlim  48891  uspgrsprfo  48946  funcringcsetcALTV2lem8  49095  funcringcsetclem8ALTV  49118  itcovalendof  49482  tposidf1o  49698  idfu1stf1o  49910  imaidfu  49921  idfth  49969  idsubc  49971  fucoppc  50221  oduoppcciso  50377