Theorem f1oi 6812

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6621	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6524	. . . 4 ⊢ Fun I
3		cnvi 6099	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6513	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 231	. . 3 ⊢ Fun ◡ I
6		funres11 6569	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6034	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6779	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1343	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1542   I cid 5518  ^◡ccnv 5623  ran crn 5625   ↾ cres 5626  Fun wfun 6486   Fn wfn 6487  –1-1-onto→wf1o 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  f1ovi  6814  fveqf1o  7250  f1ofvswap  7254  isoid  7277  enrefg  8924  ssdomg  8940  enreffi  9110  ssdomfi  9123  ssdomfi2  9124  wdomref  9480  infxpenc  9931  pwfseqlem5  10577  fproddvdsd  16295  wunndx  17156  idfucl  17839  idffth  17893  ressffth  17898  setccatid  18042  estrccatid  18089  funcestrcsetclem7  18103  funcestrcsetclem8  18104  equivestrcsetc  18109  funcsetcestrclem7  18118  funcsetcestrclem8  18119  idmgmhm  18660  idmhm  18754  ielefmnd  18846  sursubmefmnd  18855  injsubmefmnd  18856  idghm  19197  idresperm  19352  islinds2  21803  lindfres  21813  lindsmm  21818  mdetunilem9  22595  ssidcn  23230  resthauslem  23338  sshauslem  23347  idqtop  23681  fmid  23935  iducn  24257  mbfid  25612  dvid  25895  dvexp  25930  wilthlem2  27046  wilthlem3  27047  idmot  28619  ausgrusgrb  29248  upgrres1  29396  umgrres1  29397  usgrres1  29398  usgrexilem  29523  sizusglecusglem1  29545  pliguhgr  30572  hoif  31840  idunop  32064  idcnop  32067  elunop2  32099  fcobijfs  32809  fcobijfs2  32810  symgcom  33159  fzo0pmtrlast  33168  pmtridf1o  33170  cycpmfvlem  33188  cycpmfv3  33191  cycpmcl  33192  islinds5  33442  ellspds  33443  qqhre  34180  rrhre  34181  subfacp1lem4  35381  subfacp1lem5  35382  poimirlem15  37970  poimirlem22  37977  idlaut  40556  tendoidcl  41229  tendo0co2  41248  erng1r  41455  dvalveclem  41485  dva0g  41487  dvh0g  41571  mzpresrename  43196  eldioph2lem1  43206  eldioph2lem2  43207  diophren  43259  kelac2  43511  lnrfg  43565  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjimaid  47883  grimidvtxedg  48373  ushggricedg  48415  stgrusgra  48447  grlicref  48500  gpgusgra  48545  gpg5grlim  48581  uspgrsprfo  48636  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  itcovalendof  49157  tposidf1o  49374  idfu1stf1o  49586  imaidfu  49597  idfth  49645  idsubc  49647  fucoppc  49897  oduoppcciso  50053