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

Theorem f1oi 5866
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  |`  A ) : A -1-1-onto-> A

Proof of Theorem f1oi
StepHypRef Expression
1 fnresi 5711 . 2  |-  (  _I  |`  A )  Fn  A
2 cnvresid 5671 . . . 4  |-  `' (  _I  |`  A )  =  (  _I  |`  A )
32fneq1i 5688 . . 3  |-  ( `' (  _I  |`  A )  Fn  A  <->  (  _I  |`  A )  Fn  A
)
41, 3mpbir 212 . 2  |-  `' (  _I  |`  A )  Fn  A
5 dff1o4 5839 . 2  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A )  Fn  A  /\  `' (  _I  |`  A )  Fn  A ) )
61, 4, 5mpbir2an 928 1  |-  (  _I  |`  A ) : A -1-1-onto-> A
Colors of variables: wff setvar class
Syntax hints:    _I cid 4764   `'ccnv 4853    |` cres 4856    Fn wfn 5596   -1-1-onto->wf1o 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608
This theorem is referenced by:  f1ovi  5867  fveqf1o  6215  isoid  6235  enrefg  7608  ssdomg  7622  hartogslem1  8057  wdomref  8087  infxpenc  8447  pwfseqlem5  9087  dfle2  11446  wunndx  15100  idfucl  15737  idffth  15789  ressffth  15794  setccatid  15930  estrccatid  15968  funcestrcsetclem7  15982  funcestrcsetclem8  15983  equivestrcsetc  15988  funcsetcestrclem7  15997  funcsetcestrclem8  15998  idmhm  16542  idghm  16849  symggrp  16992  symgid  16993  idresperm  17001  islinds2  19302  lindfres  19312  lindsmm  19317  mdetunilem9  19576  ssidcn  20202  resthauslem  20310  sshauslem  20319  hausdiag  20591  idqtop  20652  fmid  20906  iducn  21229  mbfid  22469  dvid  22749  dvexp  22784  wilthlem2  23859  wilthlem3  23860  idmot  24442  ausisusgra  24928  cusgraexilem2  25040  sizeusglecusglem1  25057  hoif  27242  idunop  27466  idcnop  27469  elunop2  27501  fcobijfs  28154  qqhre  28663  rrhre  28664  subfacp1lem4  29694  subfacp1lem5  29695  ghomsn  30094  poimirlem15  31659  poimirlem22  31666  idlaut  33370  tendoidcl  34045  tendo0co2  34064  erng1r  34271  dvalveclem  34302  dva0g  34304  dvh0g  34388  mzpresrename  35301  eldioph2lem1  35311  eldioph2lem2  35312  diophren  35365  kelac2  35629  lnrfg  35684  usgresvm1  38513  usgresvm1ALT  38517  idmgmhm  38546  funcringcsetcALTV2lem8  38803  funcringcsetclem8ALTV  38826
  Copyright terms: Public domain W3C validator