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

Theorem fcoi1 5610
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 5584 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 df-fn 5450 . . 3  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
3 eqimss 3393 . . . . 5  |-  ( dom 
F  =  A  ->  dom  F  C_  A )
4 cnvi 5269 . . . . . . . . . 10  |-  `'  _I  =  _I
54reseq1i 5135 . . . . . . . . 9  |-  ( `'  _I  |`  A )  =  (  _I  |`  A )
65cnveqi 5040 . . . . . . . 8  |-  `' ( `'  _I  |`  A )  =  `' (  _I  |`  A )
7 cnvresid 5516 . . . . . . . 8  |-  `' (  _I  |`  A )  =  (  _I  |`  A )
86, 7eqtr2i 2457 . . . . . . 7  |-  (  _I  |`  A )  =  `' ( `'  _I  |`  A )
98coeq2i 5026 . . . . . 6  |-  ( F  o.  (  _I  |`  A ) )  =  ( F  o.  `' ( `'  _I  |`  A )
)
10 cores2 5375 . . . . . 6  |-  ( dom 
F  C_  A  ->  ( F  o.  `' ( `'  _I  |`  A )
)  =  ( F  o.  _I  ) )
119, 10syl5eq 2480 . . . . 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 5464 . . . . 5  |-  ( Fun 
F  ->  Rel  F )
14 coi1 5378 . . . . 5  |-  ( Rel 
F  ->  ( F  o.  _I  )  =  F )
1513, 14syl 16 . . . 4  |-  ( Fun 
F  ->  ( F  o.  _I  )  =  F )
1612, 15sylan9eqr 2490 . . 3  |-  ( ( Fun  F  /\  dom  F  =  A )  -> 
( F  o.  (  _I  |`  A ) )  =  F )
172, 16sylbi 188 . 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 set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    C_ wss 3313    _I cid 4486   `'ccnv 4870   dom cdm 4871    |` cres 4873    o. ccom 4875   Rel wrel 4876   Fun wfun 5441    Fn wfn 5442   -->wf 5443
This theorem is referenced by:  fcof1o  6019  mapen  7264  mapfien  7646  hashfacen  11696  cofurid  14081  setccatid  14232  curf2ndf  14337  symgid  15097  pf1mpf  19965  pf1ind  19968  wilthlem3  20846  hoico1  23252  diophrw  26809  f1omvdco2  27360  psgnunilem1  27385  mendrng  27469  ltrncoidN  30863  trlcoabs2N  31457  trlcoat  31458  cdlemg47a  31469  cdlemg46  31470  trljco  31475  tendo1mulr  31506  tendo0co2  31523  cdlemi2  31554  cdlemk2  31567  cdlemk4  31569  cdlemk8  31573  cdlemk53  31692  cdlemk55a  31694  dvhopN  31852  dihopelvalcpre  31984  dihmeetlem1N  32026  dihglblem5apreN  32027
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pr 4396
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-br 4206  df-opab 4260  df-id 4491  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-fun 5449  df-fn 5450  df-f 5451
  Copyright terms: Public domain W3C validator