MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1oi Structured version   Visualization version   GIF version

Theorem f1oi 6212
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.)
Assertion
Ref Expression
f1oi ( I ↾ 𝐴):𝐴1-1-onto𝐴

Proof of Theorem f1oi
StepHypRef Expression
1 fnresi 6046 . 2 ( I ↾ 𝐴) Fn 𝐴
2 cnvresid 6006 . . . 4 ( I ↾ 𝐴) = ( I ↾ 𝐴)
32fneq1i 6023 . . 3 (( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
41, 3mpbir 221 . 2 ( I ↾ 𝐴) Fn 𝐴
5 dff1o4 6183 . 2 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴( I ↾ 𝐴) Fn 𝐴))
61, 4, 5mpbir2an 975 1 ( I ↾ 𝐴):𝐴1-1-onto𝐴
Colors of variables: wff setvar class
Syntax hints:   I cid 5052  ccnv 5142  cres 5145   Fn wfn 5921  1-1-ontowf1o 5925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933
This theorem is referenced by:  f1ovi  6213  fveqf1o  6597  isoid  6619  enrefg  8029  ssdomg  8043  hartogslem1  8488  wdomref  8518  infxpenc  8879  pwfseqlem5  9523  dfle2  12018  fproddvdsd  15106  wunndx  15925  idfucl  16588  idffth  16640  ressffth  16645  setccatid  16781  estrccatid  16819  funcestrcsetclem7  16833  funcestrcsetclem8  16834  equivestrcsetc  16839  funcsetcestrclem7  16848  funcsetcestrclem8  16849  idmhm  17391  idghm  17722  symggrp  17866  symgid  17867  idresperm  17875  islinds2  20200  lindfres  20210  lindsmm  20215  mdetunilem9  20474  ssidcn  21107  resthauslem  21215  sshauslem  21224  hausdiag  21496  idqtop  21557  fmid  21811  iducn  22134  mbfid  23448  dvid  23726  dvexp  23761  wilthlem2  24840  wilthlem3  24841  idmot  25477  ausgrusgrb  26105  upgrres1  26250  umgrres1  26251  usgrres1  26252  usgrexilem  26392  sizusglecusglem1  26413  pliguhgr  27468  hoif  28741  idunop  28965  idcnop  28968  elunop2  29000  fcobijfs  29629  pmtridf1o  29984  qqhre  30192  rrhre  30193  subfacp1lem4  31291  subfacp1lem5  31292  poimirlem15  33554  poimirlem22  33561  idlaut  35700  tendoidcl  36374  tendo0co2  36393  erng1r  36600  dvalveclem  36631  dva0g  36633  dvh0g  36717  mzpresrename  37630  eldioph2lem1  37640  eldioph2lem2  37641  diophren  37694  kelac2  37952  lnrfg  38006  uspgrsprfo  42081  idmgmhm  42113  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391
  Copyright terms: Public domain W3C validator