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

Theorem f1oi 5851
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 5698 . 2  |-  (  _I  |`  A )  Fn  A
2 cnvresid 5658 . . . 4  |-  `' (  _I  |`  A )  =  (  _I  |`  A )
32fneq1i 5675 . . 3  |-  ( `' (  _I  |`  A )  Fn  A  <->  (  _I  |`  A )  Fn  A
)
41, 3mpbir 209 . 2  |-  `' (  _I  |`  A )  Fn  A
5 dff1o4 5824 . 2  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A )  Fn  A  /\  `' (  _I  |`  A )  Fn  A ) )
61, 4, 5mpbir2an 918 1  |-  (  _I  |`  A ) : A -1-1-onto-> A
Colors of variables: wff setvar class
Syntax hints:    _I cid 4790   `'ccnv 4998    |` cres 5001    Fn wfn 5583   -1-1-onto->wf1o 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595
This theorem is referenced by:  f1ovi  5852  fveqf1o  6193  isoid  6213  enrefg  7547  ssdomg  7561  hartogslem1  7967  wdomref  7998  infxpenc  8395  infxpencOLD  8400  pwfseqlem5  9041  dfle2  11353  wunndx  14506  idfucl  15108  idffth  15160  ressffth  15165  setccatid  15269  idghm  16087  symggrp  16230  symgid  16231  idresperm  16239  islinds2  18643  lindfres  18653  lindsmm  18658  mdetunilem9  18917  ssidcn  19550  resthauslem  19658  sshauslem  19667  hausdiag  19909  idqtop  19970  fmid  20224  iducn  20549  mbfid  21806  dvid  22084  dvexp  22119  wilthlem2  23099  wilthlem3  23100  idmot  23680  ausisusgra  24059  cusgraexilem2  24171  sizeusglecusglem1  24188  hoif  26377  idunop  26601  idcnop  26604  elunop2  26636  fcobijfs  27249  qqhre  27662  rrhre  27663  subfacp1lem4  28295  subfacp1lem5  28296  ghomsn  28531  mzpresrename  30315  eldioph2lem1  30325  eldioph2lem2  30326  diophren  30379  kelac2  30643  lnrfg  30700  usgresvm1  31938  usgresvm1ALT  31942  idlaut  34910  tendoidcl  35583  tendo0co2  35602  erng1r  35809  dvalveclem  35840  dva0g  35842  dvh0g  35926
  Copyright terms: Public domain W3C validator