Theorem f1oi 6818

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

Assertion

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

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6627	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		funi 6530	. . . 4 ⊢ Fun I
3		cnvi 6105	. . . . 5 ⊢ ◡ I = I
4	3	funeqi 6519	. . . 4 ⊢ (Fun ◡ I ↔ Fun I )
5	2, 4	mpbir 231	. . 3 ⊢ Fun ◡ I
6		funres11 6575	. . 3 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
7	5, 6	ax-mp 5	. 2 ⊢ Fun ◡( I ↾ 𝐴)
8		rnresi 6040	. 2 ⊢ ran ( I ↾ 𝐴) = 𝐴
9		dff1o2 6785	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ Fun ◡( I ↾ 𝐴) ∧ ran ( I ↾ 𝐴) = 𝐴))
10	1, 7, 8, 9	mpbir3an 1343	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   = wceq 1542   I cid 5525  ^◡ccnv 5630  ran crn 5632   ↾ cres 5633  Fun wfun 6492   Fn wfn 6493  –1-1-onto→wf1o 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1ovi  6820  fveqf1o  7257  f1ofvswap  7261  isoid  7284  enrefg  8931  ssdomg  8947  enreffi  9117  ssdomfi  9130  ssdomfi2  9131  wdomref  9487  infxpenc  9940  pwfseqlem5  10586  fproddvdsd  16304  wunndx  17165  idfucl  17848  idffth  17902  ressffth  17907  setccatid  18051  estrccatid  18098  funcestrcsetclem7  18112  funcestrcsetclem8  18113  equivestrcsetc  18118  funcsetcestrclem7  18127  funcsetcestrclem8  18128  idmgmhm  18669  idmhm  18763  ielefmnd  18855  sursubmefmnd  18864  injsubmefmnd  18865  idghm  19206  idresperm  19361  islinds2  21793  lindfres  21803  lindsmm  21808  mdetunilem9  22585  ssidcn  23220  resthauslem  23328  sshauslem  23337  idqtop  23671  fmid  23925  iducn  24247  mbfid  25602  dvid  25885  dvexp  25920  wilthlem2  27032  wilthlem3  27033  idmot  28605  ausgrusgrb  29234  upgrres1  29382  umgrres1  29383  usgrres1  29384  usgrexilem  29509  sizusglecusglem1  29530  pliguhgr  30557  hoif  31825  idunop  32049  idcnop  32052  elunop2  32084  fcobijfs  32794  fcobijfs2  32795  symgcom  33144  fzo0pmtrlast  33153  pmtridf1o  33155  cycpmfvlem  33173  cycpmfv3  33176  cycpmcl  33177  islinds5  33427  ellspds  33428  qqhre  34164  rrhre  34165  subfacp1lem4  35365  subfacp1lem5  35366  poimirlem15  37956  poimirlem22  37963  idlaut  40542  tendoidcl  41215  tendo0co2  41234  erng1r  41441  dvalveclem  41471  dva0g  41473  dvh0g  41557  mzpresrename  43182  eldioph2lem1  43192  eldioph2lem2  43193  diophren  43241  kelac2  43493  lnrfg  43547  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  grimidvtxedg  48361  ushggricedg  48403  stgrusgra  48435  grlicref  48488  gpgusgra  48533  gpg5grlim  48569  uspgrsprfo  48624  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  itcovalendof  49145  tposidf1o  49362  idfu1stf1o  49574  imaidfu  49585  idfth  49633  idsubc  49635  fucoppc  49885  oduoppcciso  50041