Theorem f1oi 6808

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6617	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6520	. . . 4 ⊢ Fun I
3		cnvi 6095	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6509	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 231	. . 3 ⊢ Fun ◡ I
6		funres11 6565	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6030	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6775	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1342	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1541   I cid 5515  ^◡ccnv 5620  ran crn 5622   ↾ cres 5623  Fun wfun 6482   Fn wfn 6483  –1-1-onto→wf1o 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495

This theorem is referenced by:  f1ovi  6810  fveqf1o  7244  f1ofvswap  7248  isoid  7271  enrefg  8915  ssdomg  8931  enreffi  9101  ssdomfi  9114  ssdomfi2  9115  wdomref  9467  infxpenc  9918  pwfseqlem5  10563  fproddvdsd  16250  wunndx  17110  idfucl  17792  idffth  17846  ressffth  17851  setccatid  17995  estrccatid  18042  funcestrcsetclem7  18056  funcestrcsetclem8  18057  equivestrcsetc  18062  funcsetcestrclem7  18071  funcsetcestrclem8  18072  idmgmhm  18613  idmhm  18707  ielefmnd  18799  sursubmefmnd  18808  injsubmefmnd  18809  idghm  19147  idresperm  19302  islinds2  21754  lindfres  21764  lindsmm  21769  mdetunilem9  22538  ssidcn  23173  resthauslem  23281  sshauslem  23290  idqtop  23624  fmid  23878  iducn  24200  mbfid  25566  dvid  25849  dvexp  25887  wilthlem2  27009  wilthlem3  27010  idmot  28518  ausgrusgrb  29147  upgrres1  29295  umgrres1  29296  usgrres1  29297  usgrexilem  29422  sizusglecusglem1  29444  pliguhgr  30470  hoif  31738  idunop  31962  idcnop  31965  elunop2  31997  fcobijfs  32710  fcobijfs2  32711  symgcom  33061  fzo0pmtrlast  33070  pmtridf1o  33072  cycpmfvlem  33090  cycpmfv3  33093  cycpmcl  33094  islinds5  33341  ellspds  33342  qqhre  34056  rrhre  34057  subfacp1lem4  35250  subfacp1lem5  35251  poimirlem15  37698  poimirlem22  37705  idlaut  40218  tendoidcl  40891  tendo0co2  40910  erng1r  41117  dvalveclem  41147  dva0g  41149  dvh0g  41233  mzpresrename  42870  eldioph2lem1  42880  eldioph2lem2  42881  diophren  42933  kelac2  43185  lnrfg  43239  fundcmpsurbijinjpreimafv  47534  fundcmpsurinjimaid  47538  grimidvtxedg  48012  ushggricedg  48054  stgrusgra  48086  grlicref  48139  gpgusgra  48184  gpg5grlim  48220  uspgrsprfo  48275  funcringcsetcALTV2lem8  48424  funcringcsetclem8ALTV  48447  itcovalendof  48797  tposidf1o  49014  idfu1stf1o  49227  imaidfu  49238  idfth  49286  idsubc  49288  fucoppc  49538  oduoppcciso  49694