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

Theorem fcoi1 5752
Description: Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fcoi1  |-  ( F : A --> B  -> 
( F  o.  (  _I  |`  A ) )  =  F )

Proof of Theorem fcoi1
StepHypRef Expression
1 ffn 5724 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 df-fn 5584 . . 3  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
3 eqimss 3551 . . . . 5  |-  ( dom 
F  =  A  ->  dom  F  C_  A )
4 cnvi 5403 . . . . . . . . . 10  |-  `'  _I  =  _I
54reseq1i 5262 . . . . . . . . 9  |-  ( `'  _I  |`  A )  =  (  _I  |`  A )
65cnveqi 5170 . . . . . . . 8  |-  `' ( `'  _I  |`  A )  =  `' (  _I  |`  A )
7 cnvresid 5651 . . . . . . . 8  |-  `' (  _I  |`  A )  =  (  _I  |`  A )
86, 7eqtr2i 2492 . . . . . . 7  |-  (  _I  |`  A )  =  `' ( `'  _I  |`  A )
98coeq2i 5156 . . . . . 6  |-  ( F  o.  (  _I  |`  A ) )  =  ( F  o.  `' ( `'  _I  |`  A )
)
10 cores2 5513 . . . . . 6  |-  ( dom 
F  C_  A  ->  ( F  o.  `' ( `'  _I  |`  A )
)  =  ( F  o.  _I  ) )
119, 10syl5eq 2515 . . . . 5  |-  ( dom 
F  C_  A  ->  ( F  o.  (  _I  |`  A ) )  =  ( F  o.  _I  ) )
123, 11syl 16 . . . 4  |-  ( dom 
F  =  A  -> 
( F  o.  (  _I  |`  A ) )  =  ( F  o.  _I  ) )
13 funrel 5598 . . . . 5  |-  ( Fun 
F  ->  Rel  F )
14 coi1 5516 . . . . 5  |-  ( Rel 
F  ->  ( F  o.  _I  )  =  F )
1513, 14syl 16 . . . 4  |-  ( Fun 
F  ->  ( F  o.  _I  )  =  F )
1612, 15sylan9eqr 2525 . . 3  |-  ( ( Fun  F  /\  dom  F  =  A )  -> 
( F  o.  (  _I  |`  A ) )  =  F )
172, 16sylbi 195 . 2  |-  ( F  Fn  A  ->  ( F  o.  (  _I  |`  A ) )  =  F )
181, 17syl 16 1  |-  ( F : A --> B  -> 
( F  o.  (  _I  |`  A ) )  =  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    C_ wss 3471    _I cid 4785   `'ccnv 4993   dom cdm 4994    |` cres 4996    o. ccom 4998   Rel wrel 4999   Fun wfun 5575    Fn wfn 5576   -->wf 5577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443  df-opab 4501  df-id 4790  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-fun 5583  df-fn 5584  df-f 5585
This theorem is referenced by:  fcof1oinvd  6177  mapen  7673  mapfien  7858  mapfienOLD  8129  hashfacen  12458  cofurid  15109  setccatid  15260  curf2ndf  15365  symgid  16216  f1omvdco2  16264  psgnunilem1  16309  pf1mpf  18154  pf1ind  18157  wilthlem3  23067  hoico1  26339  fcobijfs  27209  diophrw  30285  mendrng  30737  ltrncoidN  34801  trlcoabs2N  35395  trlcoat  35396  cdlemg47a  35407  cdlemg46  35408  trljco  35413  tendo1mulr  35444  tendo0co2  35461  cdlemi2  35492  cdlemk2  35505  cdlemk4  35507  cdlemk8  35511  cdlemk53  35630  cdlemk55a  35632  dvhopN  35790  dihopelvalcpre  35922  dihmeetlem1N  35964  dihglblem5apreN  35965
  Copyright terms: Public domain W3C validator