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

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

Proof of Theorem fcoi2
StepHypRef Expression
1 df-f 5604 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
2 cores 5356 . . 3  |-  ( ran 
F  C_  B  ->  ( (  _I  |`  B )  o.  F )  =  (  _I  o.  F
) )
3 fnrel 5695 . . . 4  |-  ( F  Fn  A  ->  Rel  F )
4 coi2 5370 . . . 4  |-  ( Rel 
F  ->  (  _I  o.  F )  =  F )
53, 4syl 17 . . 3  |-  ( F  Fn  A  ->  (  _I  o.  F )  =  F )
62, 5sylan9eqr 2517 . 2  |-  ( ( F  Fn  A  /\  ran  F  C_  B )  ->  ( (  _I  |`  B )  o.  F )  =  F )
71, 6sylbi 200 1  |-  ( F : A --> B  -> 
( (  _I  |`  B )  o.  F )  =  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1454    C_ wss 3415    _I cid 4762   ran crn 4853    |` cres 4854    o. ccom 4856   Rel wrel 4857    Fn wfn 5595   -->wf 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-fun 5602  df-fn 5603  df-f 5604
This theorem is referenced by:  fcof1oinvd  6215  mapen  7761  mapfien  7946  hashfacen  12649  cofulid  15843  setccatid  16027  estrccatid  16065  symggrp  17089  f1omvdco2  17137  symggen  17159  psgnunilem1  17182  gsumval3  17589  gsumzf1o  17594  frgpcyg  19192  f1linds  19431  qtophmeo  20880  motgrp  24636  hoico2  27458  fcoinver  28262  fcobij  28358  symgfcoeu  28656  subfacp1lem5  29955  ltrncoidN  33737  trlcoat  34334  trlcone  34339  cdlemg47a  34345  cdlemg47  34347  trljco  34351  tgrpgrplem  34360  tendo1mul  34381  tendo0pl  34402  cdlemkid2  34535  cdlemk45  34558  cdlemk53b  34567  erng1r  34606  tendocnv  34633  dvalveclem  34637  dva0g  34639  dvhgrp  34719  dvhlveclem  34720  dvh0g  34723  cdlemn8  34816  dihordlem7b  34827  dihopelvalcpre  34860  mendring  36102  rngccatidALTV  40263  ringccatidALTV  40326
  Copyright terms: Public domain W3C validator