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

Theorem f1oi 6643
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 6465 . 2 ( I ↾ 𝐴) Fn 𝐴
2 cnvresid 6421 . . . 4 ( I ↾ 𝐴) = ( I ↾ 𝐴)
32fneq1i 6438 . . 3 (( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
41, 3mpbir 234 . 2 ( I ↾ 𝐴) Fn 𝐴
5 dff1o4 6614 . 2 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴( I ↾ 𝐴) Fn 𝐴))
61, 4, 5mpbir2an 710 1 ( I ↾ 𝐴):𝐴1-1-onto𝐴
Colors of variables: wff setvar class
Syntax hints:   I cid 5446  ccnv 5541  cres 5544   Fn wfn 6338  1-1-ontowf1o 6342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-br 5053  df-opab 5115  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350
This theorem is referenced by:  f1ovi  6644  fveqf1o  7051  isoid  7075  enrefg  8537  ssdomg  8551  wdomref  9033  infxpenc  9442  pwfseqlem5  10083  fproddvdsd  15684  wunndx  16504  idfucl  17151  idffth  17203  ressffth  17208  setccatid  17344  estrccatid  17382  funcestrcsetclem7  17396  funcestrcsetclem8  17397  equivestrcsetc  17402  funcsetcestrclem7  17411  funcsetcestrclem8  17412  idmhm  17965  ielefmnd  18052  sursubmefmnd  18061  injsubmefmnd  18062  idghm  18373  idresperm  18514  islinds2  20957  lindfres  20967  lindsmm  20972  mdetunilem9  21229  ssidcn  21863  resthauslem  21971  sshauslem  21980  idqtop  22314  fmid  22568  iducn  22892  mbfid  24242  dvid  24524  dvexp  24559  wilthlem2  25657  wilthlem3  25658  idmot  26334  ausgrusgrb  26961  upgrres1  27106  umgrres1  27107  usgrres1  27108  usgrexilem  27233  sizusglecusglem1  27254  pliguhgr  28272  hoif  29540  idunop  29764  idcnop  29767  elunop2  29799  fcobijfs  30470  symgcom  30759  pmtridf1o  30768  cycpmfvlem  30786  cycpmfv3  30789  cycpmcl  30790  islinds5  30965  ellspds  30966  qqhre  31318  rrhre  31319  subfacp1lem4  32487  subfacp1lem5  32488  poimirlem15  35017  poimirlem22  35024  idlaut  37337  tendoidcl  38010  tendo0co2  38029  erng1r  38236  dvalveclem  38266  dva0g  38268  dvh0g  38352  mzpresrename  39607  eldioph2lem1  39617  eldioph2lem2  39618  diophren  39670  kelac2  39925  lnrfg  39979  fundcmpsurbijinjpreimafv  43850  fundcmpsurinjimaid  43854  isomgreqve  44269  ushrisomgr  44285  uspgrsprfo  44302  idmgmhm  44334  funcringcsetcALTV2lem8  44593  funcringcsetclem8ALTV  44616  itcovalendof  45009
  Copyright terms: Public domain W3C validator