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

Theorem f1oi 6315
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 6148 . 2 ( I ↾ 𝐴) Fn 𝐴
2 cnvresid 6108 . . . 4 ( I ↾ 𝐴) = ( I ↾ 𝐴)
32fneq1i 6125 . . 3 (( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
41, 3mpbir 221 . 2 ( I ↾ 𝐴) Fn 𝐴
5 dff1o4 6286 . 2 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴( I ↾ 𝐴) Fn 𝐴))
61, 4, 5mpbir2an 682 1 ( I ↾ 𝐴):𝐴1-1-onto𝐴
Colors of variables: wff setvar class
Syntax hints:   I cid 5156  ccnv 5248  cres 5251   Fn wfn 6026  1-1-ontowf1o 6030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038
This theorem is referenced by:  f1ovi  6316  fveqf1o  6700  isoid  6722  enrefg  8141  ssdomg  8155  hartogslem1  8603  wdomref  8633  infxpenc  9041  pwfseqlem5  9687  dfle2  12185  fproddvdsd  15267  wunndx  16085  idfucl  16748  idffth  16800  ressffth  16805  setccatid  16941  estrccatid  16979  funcestrcsetclem7  16994  funcestrcsetclem8  16995  equivestrcsetc  17000  funcsetcestrclem7  17009  funcsetcestrclem8  17010  idmhm  17552  idghm  17883  symggrp  18027  symgid  18028  idresperm  18036  islinds2  20369  lindfres  20379  lindsmm  20384  mdetunilem9  20644  ssidcn  21280  resthauslem  21388  sshauslem  21397  hausdiag  21669  idqtop  21730  fmid  21984  iducn  22307  mbfid  23623  dvid  23901  dvexp  23936  wilthlem2  25016  wilthlem3  25017  idmot  25653  ausgrusgrb  26282  upgrres1  26428  umgrres1  26429  usgrres1  26430  usgrexilem  26571  sizusglecusglem1  26592  pliguhgr  27680  hoif  28953  idunop  29177  idcnop  29180  elunop2  29212  fcobijfs  29841  pmtridf1o  30196  qqhre  30404  rrhre  30405  subfacp1lem4  31503  subfacp1lem5  31504  poimirlem15  33757  poimirlem22  33764  idlaut  35904  tendoidcl  36578  tendo0co2  36597  erng1r  36804  dvalveclem  36835  dva0g  36837  dvh0g  36921  mzpresrename  37839  eldioph2lem1  37849  eldioph2lem2  37850  diophren  37903  kelac2  38161  lnrfg  38215  uspgrsprfo  42284  idmgmhm  42316  funcringcsetcALTV2lem8  42571  funcringcsetclem8ALTV  42594
  Copyright terms: Public domain W3C validator