Theorem f1oi 6820

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 6629	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6532	. . . 4 ⊢ Fun I
3		cnvi 6107	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6521	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 231	. . 3 ⊢ Fun ◡ I
6		funres11 6577	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6042	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6787	. 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 5526  ^◡ccnv 5631  ran crn 5633   ↾ cres 5634  Fun wfun 6494   Fn wfn 6495  –1-1-onto→wf1o 6499

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1ovi  6822  fveqf1o  7258  f1ofvswap  7262  isoid  7285  enrefg  8933  ssdomg  8949  enreffi  9119  ssdomfi  9132  ssdomfi2  9133  wdomref  9489  infxpenc  9940  pwfseqlem5  10586  fproddvdsd  16274  wunndx  17134  idfucl  17817  idffth  17871  ressffth  17876  setccatid  18020  estrccatid  18067  funcestrcsetclem7  18081  funcestrcsetclem8  18082  equivestrcsetc  18087  funcsetcestrclem7  18096  funcsetcestrclem8  18097  idmgmhm  18638  idmhm  18732  ielefmnd  18824  sursubmefmnd  18833  injsubmefmnd  18834  idghm  19172  idresperm  19327  islinds2  21780  lindfres  21790  lindsmm  21795  mdetunilem9  22576  ssidcn  23211  resthauslem  23319  sshauslem  23328  idqtop  23662  fmid  23916  iducn  24238  mbfid  25604  dvid  25887  dvexp  25925  wilthlem2  27047  wilthlem3  27048  idmot  28621  ausgrusgrb  29250  upgrres1  29398  umgrres1  29399  usgrres1  29400  usgrexilem  29525  sizusglecusglem1  29547  pliguhgr  30573  hoif  31841  idunop  32065  idcnop  32068  elunop2  32100  fcobijfs  32810  fcobijfs2  32811  symgcom  33176  fzo0pmtrlast  33185  pmtridf1o  33187  cycpmfvlem  33205  cycpmfv3  33208  cycpmcl  33209  islinds5  33459  ellspds  33460  qqhre  34197  rrhre  34198  subfacp1lem4  35396  subfacp1lem5  35397  poimirlem15  37883  poimirlem22  37890  idlaut  40469  tendoidcl  41142  tendo0co2  41161  erng1r  41368  dvalveclem  41398  dva0g  41400  dvh0g  41484  mzpresrename  43104  eldioph2lem1  43114  eldioph2lem2  43115  diophren  43167  kelac2  43419  lnrfg  43473  fundcmpsurbijinjpreimafv  47764  fundcmpsurinjimaid  47768  grimidvtxedg  48242  ushggricedg  48284  stgrusgra  48316  grlicref  48369  gpgusgra  48414  gpg5grlim  48450  uspgrsprfo  48505  funcringcsetcALTV2lem8  48654  funcringcsetclem8ALTV  48677  itcovalendof  49026  tposidf1o  49243  idfu1stf1o  49455  imaidfu  49466  idfth  49514  idsubc  49516  fucoppc  49766  oduoppcciso  49922