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

Theorem f1oi 5654
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 5503 . 2  |-  (  _I  |`  A )  Fn  A
2 cnvresid 5464 . . . 4  |-  `' (  _I  |`  A )  =  (  _I  |`  A )
32fneq1i 5480 . . 3  |-  ( `' (  _I  |`  A )  Fn  A  <->  (  _I  |`  A )  Fn  A
)
41, 3mpbir 201 . 2  |-  `' (  _I  |`  A )  Fn  A
5 dff1o4 5623 . 2  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A )  Fn  A  /\  `' (  _I  |`  A )  Fn  A ) )
61, 4, 5mpbir2an 887 1  |-  (  _I  |`  A ) : A -1-1-onto-> A
Colors of variables: wff set class
Syntax hints:    _I cid 4435   `'ccnv 4818    |` cres 4821    Fn wfn 5390   -1-1-onto->wf1o 5394
This theorem is referenced by:  f1ovi  5655  fveqf1o  5969  isoid  5989  enrefg  7076  ssdomg  7090  hartogslem1  7445  wdomref  7474  infxpenc  7833  pwfseqlem5  8472  dfle2  10673  wunndx  13413  idfucl  14006  idffth  14058  ressffth  14063  setccatid  14167  idghm  14949  symggrp  15031  symgid  15032  ssidcn  17242  resthauslem  17350  sshauslem  17359  hausdiag  17599  idqtop  17660  fmid  17914  iducn  18235  mbfid  19396  dvid  19672  dvexp  19707  wilthlem2  20720  wilthlem3  20721  ausisusgra  21248  cusgraexilem2  21343  sizeusglecusglem1  21360  hoif  23106  idunop  23330  idcnop  23333  elunop2  23365  qqhre  24183  rrhre  24184  subfacp1lem4  24649  subfacp1lem5  24650  ghomsn  24879  mzpresrename  26499  eldioph2lem1  26510  eldioph2lem2  26511  diophren  26566  kelac2  26833  islinds2  26953  lindfres  26963  lindsmm  26968  lnrfg  26993  idlaut  30211  tendoidcl  30884  tendo0co2  30903  erng1r  31110  dvalveclem  31141  dva0g  31143  dvh0g  31227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-br 4155  df-opab 4209  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402
  Copyright terms: Public domain W3C validator