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

Theorem fcoi2 6329
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 (𝐹:𝐴𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Proof of Theorem fcoi2
StepHypRef Expression
1 df-f 6139 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 cores 5892 . . 3 (ran 𝐹𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3 fnrel 6234 . . . 4 (𝐹 Fn 𝐴 → Rel 𝐹)
4 coi2 5906 . . . 4 (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
53, 4syl 17 . . 3 (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
62, 5sylan9eqr 2836 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
71, 6sylbi 209 1 (𝐹:𝐴𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wss 3792   I cid 5260  ran crn 5356  cres 5357  ccom 5359  Rel wrel 5360   Fn wfn 6130  wf 6131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-fun 6137  df-fn 6138  df-f 6139
This theorem is referenced by:  fcof1oinvd  6820  mapen  8412  mapfien  8601  hashfacen  13552  cofulid  16935  setccatid  17119  estrccatid  17157  symggrp  18203  f1omvdco2  18251  symggen  18273  psgnunilem1  18296  gsumval3  18694  gsumzf1o  18699  frgpcyg  20317  f1linds  20568  qtophmeo  22029  motgrp  25894  hoico2  29188  fcoinver  29981  fcobij  30066  symgfcoeu  30443  subfacp1lem5  31765  ltrncoidN  36282  trlcoat  36877  trlcone  36882  cdlemg47a  36888  cdlemg47  36890  trljco  36894  tgrpgrplem  36903  tendo1mul  36924  tendo0pl  36945  cdlemkid2  37078  cdlemk45  37101  cdlemk53b  37110  erng1r  37149  tendocnv  37175  dvalveclem  37179  dva0g  37181  dvhgrp  37261  dvhlveclem  37262  dvh0g  37265  cdlemn8  37358  dihordlem7b  37369  dihopelvalcpre  37402  mendring  38721  rngccatidALTV  43004  ringccatidALTV  43067
  Copyright terms: Public domain W3C validator