Theorem f1oi 6839

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6644	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6547	. . . 4 ⊢ Fun I
3		cnvi 5853	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6536	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 233	. . 3 ⊢ Fun ◡ I
6		funres11 6592	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6059	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6806	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1354	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1559   I cid 5537  ^◡ccnv 5642  ran crn 5644   ↾ cres 5645  Fun wfun 6509   Fn wfn 6510  –1-1-onto→wf1o 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522

This theorem is referenced by:  f1ovi  6841  fveqf1o  7280  f1ofvswap  7284  isoid  7307  enrefg  8958  ssdomg  8974  enreffi  9144  ssdomfi  9157  ssdomfi2  9158  wdomref  9513  infxpenc  9967  pwfseqlem5  10614  fproddvdsd  16359  wunndx  17221  idfucl  17904  idffth  17958  ressffth  17963  setccatid  18107  estrccatid  18154  funcestrcsetclem7  18168  funcestrcsetclem8  18169  equivestrcsetc  18174  funcsetcestrclem7  18183  funcsetcestrclem8  18184  idmgmhm  18725  idmhm  18819  ielefmnd  18911  sursubmefmnd  18920  injsubmefmnd  18921  idghm  19261  idresperm  19416  islinds2  21852  lindfres  21862  lindsmm  21867  mdetunilem9  22667  ssidcn  23302  resthauslem  23410  sshauslem  23419  idqtop  23753  fmid  24007  iducn  24329  mbfid  25684  dvid  25967  dvexp  26002  wilthlem2  27120  wilthlem3  27121  idmot  28693  ausgrusgrb  29322  upgrres1  29470  umgrres1  29471  usgrres1  29472  usgrexilem  29597  sizusglecusglem1  29618  pliguhgr  30645  hoif  31913  idunop  32137  idcnop  32140  elunop2  32172  fcobijfs  32883  fcobijfs2  32884  symgcom  33223  fzo0pmtrlast  33232  pmtridf1o  33234  cycpmfvlem  33252  cycpmfv3  33255  cycpmcl  33256  islinds5  33513  ellspds  33514  qqhre  34277  rrhre  34278  subfacp1lem4  35493  subfacp1lem5  35494  poimirlem15  38094  poimirlem22  38101  idlaut  40680  tendoidcl  41353  tendo0co2  41372  erng1r  41579  dvalveclem  41609  dva0g  41611  dvh0g  41695  mzpresrename  43291  eldioph2lem1  43301  eldioph2lem2  43302  diophren  43350  kelac2  43602  lnrfg  43656  fundcmpsurbijinjpreimafv  47973  fundcmpsurinjimaid  47977  grimidvtxedg  48467  ushggricedg  48509  stgrusgra  48541  grlicref  48594  gpgusgra  48639  gpg5grlim  48675  uspgrsprfo  48730  funcringcsetcALTV2lem8  48879  funcringcsetclem8ALTV  48902  itcovalendof  49251  tposidf1o  49468  idfu1stf1o  49680  imaidfu  49691  idfth  49739  idsubc  49741  fucoppc  49991  oduoppcciso  50147