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

Theorem fcoi1 6763
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 6715 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 df-fn 6544 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eqimss 4040 . . . . 5 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
4 cnvi 6139 . . . . . . . . . 10 I = I
54reseq1i 5976 . . . . . . . . 9 ( I ↾ 𝐴) = ( I ↾ 𝐴)
65cnveqi 5873 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
7 cnvresid 6625 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
86, 7eqtr2i 2762 . . . . . . 7 ( I ↾ 𝐴) = ( I ↾ 𝐴)
98coeq2i 5859 . . . . . 6 (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹( I ↾ 𝐴))
10 cores2 6256 . . . . . 6 (dom 𝐹𝐴 → (𝐹( I ↾ 𝐴)) = (𝐹 ∘ I ))
119, 10eqtrid 2785 . . . . 5 (dom 𝐹𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
123, 11syl 17 . . . 4 (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13 funrel 6563 . . . . 5 (Fun 𝐹 → Rel 𝐹)
14 coi1 6259 . . . . 5 (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
1513, 14syl 17 . . . 4 (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
1612, 15sylan9eqr 2795 . . 3 ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
172, 16sylbi 216 . 2 (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
181, 17syl 17 1 (𝐹:𝐴𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wss 3948   I cid 5573  ccnv 5675  dom cdm 5676  cres 5678  ccom 5680  Rel wrel 5681  Fun wfun 6535   Fn wfn 6536  wf 6537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6543  df-fn 6544  df-f 6545
This theorem is referenced by:  fcof1oinvd  7288  mapen  9138  mapfien  9400  hashfacen  14410  hashfacenOLD  14411  cofurid  17838  setccatid  18031  estrccatid  18080  curf2ndf  18197  efmndid  18766  efmndmnd  18767  f1omvdco2  19311  psgnunilem1  19356  pf1mpf  21863  pf1ind  21866  wilthlem3  26564  hoico1  30997  fmptco1f1o  31845  fcobijfs  31936  cycpmconjslem2  32302  cycpmconjs  32303  cyc3conja  32304  reprpmtf1o  33627  ltrncoidN  38988  trlcoabs2N  39582  trlcoat  39583  cdlemg47a  39594  cdlemg46  39595  trljco  39600  tendo1mulr  39631  tendo0co2  39648  cdlemi2  39679  cdlemk2  39692  cdlemk4  39694  cdlemk8  39698  cdlemk53  39817  cdlemk55a  39819  dvhopN  39976  dihopelvalcpre  40108  dihmeetlem1N  40150  dihglblem5apreN  40151  diophrw  41483  mendring  41920  rngccatidALTV  46841  ringccatidALTV  46904
  Copyright terms: Public domain W3C validator