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

Theorem fcoi1 5972
Description: Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fcoi1 (𝐹:𝐴𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)

Proof of Theorem fcoi1
StepHypRef Expression
1 ffn 5940 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 df-fn 5789 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eqimss 3615 . . . . 5 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
4 cnvi 5438 . . . . . . . . . 10 I = I
54reseq1i 5296 . . . . . . . . 9 ( I ↾ 𝐴) = ( I ↾ 𝐴)
65cnveqi 5203 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
7 cnvresid 5864 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
86, 7eqtr2i 2628 . . . . . . 7 ( I ↾ 𝐴) = ( I ↾ 𝐴)
98coeq2i 5188 . . . . . 6 (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹( I ↾ 𝐴))
10 cores2 5547 . . . . . 6 (dom 𝐹𝐴 → (𝐹( I ↾ 𝐴)) = (𝐹 ∘ I ))
119, 10syl5eq 2651 . . . . 5 (dom 𝐹𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
123, 11syl 17 . . . 4 (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13 funrel 5803 . . . . 5 (Fun 𝐹 → Rel 𝐹)
14 coi1 5550 . . . . 5 (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
1513, 14syl 17 . . . 4 (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
1612, 15sylan9eqr 2661 . . 3 ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
172, 16sylbi 205 . 2 (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
181, 17syl 17 1 (𝐹:𝐴𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wss 3535   I cid 4934  ccnv 5023  dom cdm 5024  cres 5026  ccom 5028  Rel wrel 5029  Fun wfun 5780   Fn wfn 5781  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-fun 5788  df-fn 5789  df-f 5790
This theorem is referenced by:  fcof1oinvd  6422  mapen  7982  mapfien  8169  hashfacen  13043  cofurid  16316  setccatid  16499  estrccatid  16537  curf2ndf  16652  symgid  17586  f1omvdco2  17633  psgnunilem1  17678  pf1mpf  19479  pf1ind  19482  wilthlem3  24509  hoico1  27801  fcobijfs  28691  ltrncoidN  34231  trlcoabs2N  34827  trlcoat  34828  cdlemg47a  34839  cdlemg46  34840  trljco  34845  tendo1mulr  34876  tendo0co2  34893  cdlemi2  34924  cdlemk2  34937  cdlemk4  34939  cdlemk8  34943  cdlemk53  35062  cdlemk55a  35064  dvhopN  35222  dihopelvalcpre  35354  dihmeetlem1N  35396  dihglblem5apreN  35397  diophrw  36139  mendring  36580  rngccatidALTV  41779  ringccatidALTV  41842
  Copyright terms: Public domain W3C validator