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

Theorem fcoi2 6234
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 6046 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 cores 5793 . . 3 (ran 𝐹𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3 fnrel 6140 . . . 4 (𝐹 Fn 𝐴 → Rel 𝐹)
4 coi2 5807 . . . 4 (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
53, 4syl 17 . . 3 (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
62, 5sylan9eqr 2830 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
71, 6sylbi 208 1 (𝐹:𝐴𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1634  wss 3729   I cid 5170  ran crn 5264  cres 5265  ccom 5267  Rel wrel 5268   Fn wfn 6037  wf 6038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798  df-opab 4860  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-fun 6044  df-fn 6045  df-f 6046
This theorem is referenced by:  fcof1oinvd  6710  mapen  8301  mapfien  8490  hashfacen  13462  cofulid  16777  setccatid  16961  estrccatid  16999  symggrp  18047  f1omvdco2  18095  symggen  18117  psgnunilem1  18140  gsumval3  18535  gsumzf1o  18540  frgpcyg  20157  f1linds  20401  qtophmeo  21861  motgrp  25680  hoico2  28973  fcoinver  29773  fcobij  29857  symgfcoeu  30202  subfacp1lem5  31521  ltrncoidN  35952  trlcoat  36548  trlcone  36553  cdlemg47a  36559  cdlemg47  36561  trljco  36565  tgrpgrplem  36574  tendo1mul  36595  tendo0pl  36616  cdlemkid2  36749  cdlemk45  36772  cdlemk53b  36781  erng1r  36820  tendocnv  36846  dvalveclem  36850  dva0g  36852  dvhgrp  36932  dvhlveclem  36933  dvh0g  36936  cdlemn8  37029  dihordlem7b  37040  dihopelvalcpre  37073  mendring  38303  rngccatidALTV  42541  ringccatidALTV  42604
  Copyright terms: Public domain W3C validator