Theorem f1oi 6805

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6614	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6517	. . . 4 ⊢ Fun I
3		cnvi 6092	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6506	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 232	. . 3 ⊢ Fun ◡ I
6		funres11 6562	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6027	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6772	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1348	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1547   I cid 5512  ^◡ccnv 5617  ran crn 5619   ↾ cres 5620  Fun wfun 6479   Fn wfn 6480  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1ovi  6807  fveqf1o  7246  f1ofvswap  7250  isoid  7273  enrefg  8921  ssdomg  8937  enreffi  9107  ssdomfi  9120  ssdomfi2  9121  wdomref  9477  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  21788  lindfres  21798  lindsmm  21803  mdetunilem9  22603  ssidcn  23238  resthauslem  23346  sshauslem  23355  idqtop  23689  fmid  23943  iducn  24265  mbfid  25620  dvid  25903  dvexp  25938  wilthlem2  27050  wilthlem3  27051  idmot  28623  ausgrusgrb  29252  upgrres1  29400  umgrres1  29401  usgrres1  29402  usgrexilem  29527  sizusglecusglem1  29548  pliguhgr  30575  hoif  31843  idunop  32067  idcnop  32070  elunop2  32102  fcobijfs  32813  fcobijfs2  32814  symgcom  33164  fzo0pmtrlast  33173  pmtridf1o  33175  cycpmfvlem  33193  cycpmfv3  33196  cycpmcl  33197  islinds5  33450  ellspds  33451  qqhre  34204  rrhre  34205  subfacp1lem4  35411  subfacp1lem5  35412  poimirlem15  38002  poimirlem22  38009  idlaut  40588  tendoidcl  41261  tendo0co2  41280  erng1r  41487  dvalveclem  41517  dva0g  41519  dvh0g  41603  mzpresrename  43199  eldioph2lem1  43209  eldioph2lem2  43210  diophren  43258  kelac2  43510  lnrfg  43564  fundcmpsurbijinjpreimafv  47882  fundcmpsurinjimaid  47886  grimidvtxedg  48376  ushggricedg  48418  stgrusgra  48450  grlicref  48503  gpgusgra  48548  gpg5grlim  48584  uspgrsprfo  48639  funcringcsetcALTV2lem8  48788  funcringcsetclem8ALTV  48811  itcovalendof  49160  tposidf1o  49377  idfu1stf1o  49589  imaidfu  49600  idfth  49648  idsubc  49650  fucoppc  49900  oduoppcciso  50056