Theorem f1oi 6894

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6698	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6600	. . . 4 ⊢ Fun I
3		cnvi 5875	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6588	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6647	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6091	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6860	. 2 ⊢ (( I ↾ 𝐴):𝐴⟶1-1onto𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1360	1 ⊢ ( I ↾ 𝐴):𝐴⟶1-1onto𝐴

This proof depends on syntax axioms:   = wceq 1570   I cid 5552  ^◡ccnv 5657  ran crn 5659   ↾ cres 5660  Fun wfun 6560   Fn wfn 6561  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1ovi  6896  fveqf1o  7341  f1ofvswap  7345  isoid  7368  enrefg  9049  ssdomg  9065  enreffi  9236  ssdomfi  9249  ssdomfi2  9250  wdomref  9603  infxpenc  10136  pwfseqlem5  10787  fproddvdsd  16549  wunndx  17417  idfucl  18106  idffth  18160  ressffth  18165  setccatid  18309  estrccatid  18356  funcestrcsetclem7  18370  funcestrcsetclem8  18371  equivestrcsetc  18376  funcsetcestrclem7  18385  funcsetcestrclem8  18386  idmgmhm  18940  idmhm  19040  ielefmnd  19133  sursubmefmnd  19142  injsubmefmnd  19143  idghm  19495  idresperm  19651  ricref  20799  islinds2  22174  lindfres  22184  lindsmm  22189  mdetunilem9  22990  ssidcn  23628  resthauslem  23736  sshauslem  23745  idqtop  24080  fmid  24334  iducn  24656  mbfid  26011  dvid  26293  dvexp  26328  wilthlem2  27453  wilthlem3  27454  idmot  29057  ausgrusgrb  29803  upgrres1  29951  umgrres1  29952  usgrres1  29953  usgrexilem  30078  sizusglecusglem1  30099  pliguhgr  31145  hoif  32413  idunop  32637  idcnop  32640  elunop2  32672  fcobijfs  33409  fcobijfs2  33410  symgcom  33743  fzo0pmtrlast  33752  pmtridf1o  33754  cycpmfvlem  33772  cycpmfv3  33775  cycpmcl  33776  islinds5  34027  ellspds  34028  qqhre  34763  rrhre  34764  subfacp1lem4  36156  subfacp1lem5  36157  poimirlem15  38821  poimirlem22  38828  idlaut  41419  tendoidcl  42092  tendo0co2  42111  erng1r  42318  dvalveclem  42348  dva0g  42350  dvh0g  42434  mzpresrename  44027  eldioph2lem1  44037  eldioph2lem2  44038  diophren  44086  kelac2  44333  lnrfg  44386  grpgimcanon  46192  fundcmpsurbijinjpreimafv  48762  fundcmpsurinjimaid  48766  grimidvtxedg  49256  ushggricedg  49298  stgrusgra  49330  grlicref  49383  gpgusgra  49428  gpg5grlim  49464  uspgrsprfo  49519  funcringcsetcALTV2lem8  49667  funcringcsetclem8ALTV  49690  itcovalendof  50112  tposidf1o  50331  idfu1stf1o  50546  imaidfu  50557  idfth  50605  idsubc  50607  fucoppc  50876  oduoppcciso  51035  parmapfunc2  51105  parmapfunc  51106