Theorem f1oi 6864

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6669	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6573	. . . 4 ⊢ Fun I
3		cnvi 5862	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6561	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6618	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6072	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6831	. 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 1569   I cid 5544  ^◡ccnv 5649  ran crn 5651   ↾ cres 5652  Fun wfun 6533   Fn wfn 6534  –1-1-onto→wf1o 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546

This theorem is used by:  f1ovi  6866  fveqf1o  7311  f1ofvswap  7315  isoid  7338  enrefg  9015  ssdomg  9031  enreffi  9202  ssdomfi  9215  ssdomfi2  9216  wdomref  9570  infxpenc  10101  pwfseqlem5  10752  fproddvdsd  16511  wunndx  17379  idfucl  18062  idffth  18116  ressffth  18121  setccatid  18265  estrccatid  18312  funcestrcsetclem7  18326  funcestrcsetclem8  18327  equivestrcsetc  18332  funcsetcestrclem7  18341  funcsetcestrclem8  18342  idmgmhm  18896  idmhm  18996  ielefmnd  19089  sursubmefmnd  19098  injsubmefmnd  19099  idghm  19451  idresperm  19606  ricref  20754  islinds2  22125  lindfres  22135  lindsmm  22140  mdetunilem9  22941  ssidcn  23579  resthauslem  23687  sshauslem  23696  idqtop  24031  fmid  24285  iducn  24607  mbfid  25962  dvid  26244  dvexp  26279  wilthlem2  27402  wilthlem3  27403  idmot  29006  ausgrusgrb  29752  upgrres1  29900  umgrres1  29901  usgrres1  29902  usgrexilem  30027  sizusglecusglem1  30048  pliguhgr  31094  hoif  32362  idunop  32586  idcnop  32589  elunop2  32621  fcobijfs  33360  fcobijfs2  33361  symgcom  33691  fzo0pmtrlast  33700  pmtridf1o  33702  cycpmfvlem  33720  cycpmfv3  33723  cycpmcl  33724  islinds5  33970  ellspds  33971  qqhre  34699  rrhre  34700  subfacp1lem4  36035  subfacp1lem5  36036  poimirlem15  38647  poimirlem22  38654  idlaut  41247  tendoidcl  41920  tendo0co2  41939  erng1r  42146  dvalveclem  42176  dva0g  42178  dvh0g  42262  mzpresrename  43855  eldioph2lem1  43865  eldioph2lem2  43866  diophren  43914  kelac2  44161  lnrfg  44215  fundcmpsurbijinjpreimafv  48583  fundcmpsurinjimaid  48587  grimidvtxedg  49077  ushggricedg  49119  stgrusgra  49151  grlicref  49204  gpgusgra  49249  gpg5grlim  49285  uspgrsprfo  49340  funcringcsetcALTV2lem8  49488  funcringcsetclem8ALTV  49511  itcovalendof  49875  tposidf1o  50094  idfu1stf1o  50309  imaidfu  50320  idfth  50368  idsubc  50370  fucoppc  50639  oduoppcciso  50798  parmapfunc2  50868  parmapfunc  50869