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

Theorem fcoi1 6782
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 6736 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 df-fn 6565 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eqimss 4053 . . . . 5 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
4 cnvi 6163 . . . . . . . . . 10 I = I
54reseq1i 5995 . . . . . . . . 9 ( I ↾ 𝐴) = ( I ↾ 𝐴)
65cnveqi 5887 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
7 cnvresid 6646 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
86, 7eqtr2i 2763 . . . . . . 7 ( I ↾ 𝐴) = ( I ↾ 𝐴)
98coeq2i 5873 . . . . . 6 (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹( I ↾ 𝐴))
10 cores2 6280 . . . . . 6 (dom 𝐹𝐴 → (𝐹( I ↾ 𝐴)) = (𝐹 ∘ I ))
119, 10eqtrid 2786 . . . . 5 (dom 𝐹𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
123, 11syl 17 . . . 4 (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13 funrel 6584 . . . . 5 (Fun 𝐹 → Rel 𝐹)
14 coi1 6283 . . . . 5 (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
1513, 14syl 17 . . . 4 (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
1612, 15sylan9eqr 2796 . . 3 ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
172, 16sylbi 217 . 2 (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
181, 17syl 17 1 (𝐹:𝐴𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wss 3962   I cid 5581  ccnv 5687  dom cdm 5688  cres 5690  ccom 5692  Rel wrel 5693  Fun wfun 6556   Fn wfn 6557  wf 6558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566
This theorem is referenced by:  fcof1oinvd  7312  mapen  9179  mapfien  9445  hashfacen  14489  cofurid  17941  setccatid  18137  estrccatid  18186  curf2ndf  18303  efmndid  18913  efmndmnd  18914  f1omvdco2  19480  psgnunilem1  19525  pf1mpf  22371  pf1ind  22374  wilthlem3  27127  hoico1  31784  fmptco1f1o  32649  fcobijfs  32740  cycpmconjslem2  33157  cycpmconjs  33158  cyc3conja  33159  1arithidomlem2  33543  reprpmtf1o  34619  ltrncoidN  40110  trlcoabs2N  40704  trlcoat  40705  cdlemg47a  40716  cdlemg46  40717  trljco  40722  tendo1mulr  40753  tendo0co2  40770  cdlemi2  40801  cdlemk2  40814  cdlemk4  40816  cdlemk8  40820  cdlemk53  40939  cdlemk55a  40941  dvhopN  41098  dihopelvalcpre  41230  dihmeetlem1N  41272  dihglblem5apreN  41273  diophrw  42746  mendring  43176  rngccatidALTV  48115  ringccatidALTV  48149
  Copyright terms: Public domain W3C validator