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 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 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 232	. . 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 1348	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1547   I cid 5519  ^◡ccnv 5624  ran crn 5626   ↾ cres 5627  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

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 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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  7253  f1ofvswap  7257  isoid  7280  enrefg  8928  ssdomg  8944  enreffi  9114  ssdomfi  9127  ssdomfi2  9128  wdomref  9484  infxpenc  9938  pwfseqlem5  10584  fproddvdsd  16302  wunndx  17163  idfucl  17846  idffth  17900  ressffth  17905  setccatid  18049  estrccatid  18096  funcestrcsetclem7  18110  funcestrcsetclem8  18111  equivestrcsetc  18116  funcsetcestrclem7  18125  funcsetcestrclem8  18126  idmgmhm  18667  idmhm  18761  ielefmnd  18853  sursubmefmnd  18862  injsubmefmnd  18863  idghm  19204  idresperm  19359  islinds2  21795  lindfres  21805  lindsmm  21810  mdetunilem9  22610  ssidcn  23245  resthauslem  23353  sshauslem  23362  idqtop  23696  fmid  23950  iducn  24272  mbfid  25627  dvid  25910  dvexp  25945  wilthlem2  27057  wilthlem3  27058  idmot  28630  ausgrusgrb  29259  upgrres1  29407  umgrres1  29408  usgrres1  29409  usgrexilem  29534  sizusglecusglem1  29555  pliguhgr  30582  hoif  31850  idunop  32074  idcnop  32077  elunop2  32109  fcobijfs  32820  fcobijfs2  32821  symgcom  33171  fzo0pmtrlast  33180  pmtridf1o  33182  cycpmfvlem  33200  cycpmfv3  33203  cycpmcl  33204  islinds5  33457  ellspds  33458  qqhre  34211  rrhre  34212  subfacp1lem4  35418  subfacp1lem5  35419  poimirlem15  38009  poimirlem22  38016  idlaut  40595  tendoidcl  41268  tendo0co2  41287  erng1r  41494  dvalveclem  41524  dva0g  41526  dvh0g  41610  mzpresrename  43206  eldioph2lem1  43216  eldioph2lem2  43217  diophren  43265  kelac2  43517  lnrfg  43571  fundcmpsurbijinjpreimafv  47889  fundcmpsurinjimaid  47893  grimidvtxedg  48383  ushggricedg  48425  stgrusgra  48457  grlicref  48510  gpgusgra  48555  gpg5grlim  48591  uspgrsprfo  48646  funcringcsetcALTV2lem8  48795  funcringcsetclem8ALTV  48818  itcovalendof  49167  tposidf1o  49384  idfu1stf1o  49596  imaidfu  49607  idfth  49655  idsubc  49657  fucoppc  49907  oduoppcciso  50063