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

Theorem fcoi2 6531
 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 6332 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 cores 6073 . . 3 (ran 𝐹𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3 fnrel 6428 . . . 4 (𝐹 Fn 𝐴 → Rel 𝐹)
4 coi2 6087 . . . 4 (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
53, 4syl 17 . . 3 (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
62, 5sylan9eqr 2858 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
71, 6sylbi 220 1 (𝐹:𝐴𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ⊆ wss 3884   I cid 5427  ran crn 5524   ↾ cres 5525   ∘ ccom 5527  Rel wrel 5528   Fn wfn 6323  ⟶wf 6324 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-fun 6330  df-fn 6331  df-f 6332 This theorem is referenced by:  fcof1oinvd  7031  mapen  8669  mapfien  8859  hashfacen  13812  cofulid  17156  setccatid  17340  estrccatid  17378  efmndid  18049  efmndmnd  18050  symggrp  18524  f1omvdco2  18572  symggen  18594  psgnunilem1  18617  gsumval3  19024  gsumzf1o  19029  frgpcyg  20269  f1linds  20518  qtophmeo  22426  motgrp  26341  hoico2  29544  fcoinver  30374  fcobij  30488  symgfcoeu  30780  symgcom  30781  pmtrcnel2  30788  cycpmconjs  30852  subfacp1lem5  32545  ltrncoidN  37423  trlcoat  38018  trlcone  38023  cdlemg47a  38029  cdlemg47  38031  trljco  38035  tgrpgrplem  38044  tendo1mul  38065  tendo0pl  38086  cdlemkid2  38219  cdlemk45  38242  cdlemk53b  38251  erng1r  38290  tendocnv  38316  dvalveclem  38320  dva0g  38322  dvhgrp  38402  dvhlveclem  38403  dvh0g  38406  cdlemn8  38499  dihordlem7b  38510  dihopelvalcpre  38543  mendring  40133  rngccatidALTV  44610  ringccatidALTV  44673
 Copyright terms: Public domain W3C validator