Theorem f1oi 6861

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6666	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6570	. . . 4 ⊢ Fun I
3		cnvi 5873	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6559	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 234	. . 3 ⊢ Fun ◡ I
6		funres11 6615	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6079	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6828	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1360	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1570   I cid 5557  ^◡ccnv 5662  ran crn 5664   ↾ cres 5665  Fun wfun 6532   Fn wfn 6533  –1-1-onto→wf1o 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is referenced by:  f1ovi  6863  fveqf1o  7302  f1ofvswap  7306  isoid  7329  enrefg  8982  ssdomg  8998  enreffi  9168  ssdomfi  9181  ssdomfi2  9182  wdomref  9535  infxpenc  10003  pwfseqlem5  10649  fproddvdsd  16394  wunndx  17256  idfucl  17939  idffth  17993  ressffth  17998  setccatid  18142  estrccatid  18189  funcestrcsetclem7  18203  funcestrcsetclem8  18204  equivestrcsetc  18209  funcsetcestrclem7  18218  funcsetcestrclem8  18219  idmgmhm  18760  idmhm  18854  ielefmnd  18947  sursubmefmnd  18956  injsubmefmnd  18957  idghm  19302  idresperm  19457  islinds2  21944  lindfres  21954  lindsmm  21959  mdetunilem9  22758  ssidcn  23393  resthauslem  23501  sshauslem  23510  idqtop  23844  fmid  24098  iducn  24420  mbfid  25775  dvid  26058  dvexp  26093  wilthlem2  27214  wilthlem3  27215  idmot  28787  ausgrusgrb  29496  upgrres1  29644  umgrres1  29645  usgrres1  29646  usgrexilem  29771  sizusglecusglem1  29792  pliguhgr  30819  hoif  32087  idunop  32311  idcnop  32314  elunop2  32346  fcobijfs  33047  fcobijfs2  33048  symgcom  33384  fzo0pmtrlast  33393  pmtridf1o  33395  cycpmfvlem  33413  cycpmfv3  33416  cycpmcl  33417  islinds5  33663  ellspds  33664  qqhre  34391  rrhre  34392  subfacp1lem4  35656  subfacp1lem5  35657  poimirlem15  38267  poimirlem22  38274  idlaut  40851  tendoidcl  41524  tendo0co2  41543  erng1r  41750  dvalveclem  41780  dva0g  41782  dvh0g  41866  mzpresrename  43464  eldioph2lem1  43474  eldioph2lem2  43475  diophren  43523  kelac2  43775  lnrfg  43829  fundcmpsurbijinjpreimafv  48139  fundcmpsurinjimaid  48143  grimidvtxedg  48633  ushggricedg  48675  stgrusgra  48707  grlicref  48760  gpgusgra  48805  gpg5grlim  48841  uspgrsprfo  48896  funcringcsetcALTV2lem8  49045  funcringcsetclem8ALTV  49068  itcovalendof  49432  tposidf1o  49648  idfu1stf1o  49860  imaidfu  49871  idfth  49919  idsubc  49921  fucoppc  50171  oduoppcciso  50327