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

Theorem fcoi2 5586
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 5422 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
2 cores 5341 . . 3  |-  ( ran 
F  C_  B  ->  ( (  _I  |`  B )  o.  F )  =  (  _I  o.  F
) )
3 fnrel 5509 . . . 4  |-  ( F  Fn  A  ->  Rel  F )
4 coi2 5354 . . . 4  |-  ( Rel 
F  ->  (  _I  o.  F )  =  F )
53, 4syl 16 . . 3  |-  ( F  Fn  A  ->  (  _I  o.  F )  =  F )
62, 5sylan9eqr 2497 . 2  |-  ( ( F  Fn  A  /\  ran  F  C_  B )  ->  ( (  _I  |`  B )  o.  F )  =  F )
71, 6sylbi 195 1  |-  ( F : A --> B  -> 
( (  _I  |`  B )  o.  F )  =  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    C_ wss 3328    _I cid 4631   ran crn 4841    |` cres 4842    o. ccom 4844   Rel wrel 4845    Fn wfn 5413   -->wf 5414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-fun 5420  df-fn 5421  df-f 5422
This theorem is referenced by:  fcof1o  5997  mapen  7475  mapfien  7657  mapfienOLD  7927  hashfacen  12207  cofulid  14800  setccatid  14952  symggrp  15905  f1omvdco2  15954  symggen  15976  psgnunilem1  15999  gsumval3OLD  16382  gsumval3  16385  gsumzf1o  16391  gsumzf1oOLD  16394  frgpcyg  18006  f1linds  18254  qtophmeo  19390  hoico2  25161  fcobij  26025  subfacp1lem5  27072  mendrng  29549  ltrncoidN  33772  trlcoat  34367  trlcone  34372  cdlemg47a  34378  cdlemg47  34380  trljco  34384  tgrpgrplem  34393  tendo1mul  34414  tendo0pl  34435  cdlemkid2  34568  cdlemk45  34591  cdlemk53b  34600  erng1r  34639  tendocnv  34666  dvalveclem  34670  dva0g  34672  dvhgrp  34752  dvhlveclem  34753  dvh0g  34756  cdlemn8  34849  dihordlem7b  34860  dihopelvalcpre  34893
  Copyright terms: Public domain W3C validator