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

Theorem fcoi1 6534
 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 6495 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 df-fn 6335 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eqimss 3973 . . . . 5 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
4 cnvi 5971 . . . . . . . . . 10 I = I
54reseq1i 5818 . . . . . . . . 9 ( I ↾ 𝐴) = ( I ↾ 𝐴)
65cnveqi 5713 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
7 cnvresid 6411 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
86, 7eqtr2i 2822 . . . . . . 7 ( I ↾ 𝐴) = ( I ↾ 𝐴)
98coeq2i 5699 . . . . . 6 (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹( I ↾ 𝐴))
10 cores2 6086 . . . . . 6 (dom 𝐹𝐴 → (𝐹( I ↾ 𝐴)) = (𝐹 ∘ I ))
119, 10syl5eq 2845 . . . . 5 (dom 𝐹𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
123, 11syl 17 . . . 4 (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13 funrel 6349 . . . . 5 (Fun 𝐹 → Rel 𝐹)
14 coi1 6089 . . . . 5 (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
1513, 14syl 17 . . . 4 (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
1612, 15sylan9eqr 2855 . . 3 ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
172, 16sylbi 220 . 2 (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
181, 17syl 17 1 (𝐹:𝐴𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ⊆ wss 3883   I cid 5428  ◡ccnv 5522  dom cdm 5523   ↾ cres 5525   ∘ ccom 5527  Rel wrel 5528  Fun wfun 6326   Fn wfn 6327  ⟶wf 6328 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 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 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 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5035  df-opab 5097  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-fun 6334  df-fn 6335  df-f 6336 This theorem is referenced by:  fcof1oinvd  7037  mapen  8683  mapfien  8874  hashfacen  13828  cofurid  17173  setccatid  17356  estrccatid  17394  curf2ndf  17509  efmndid  18065  efmndmnd  18066  f1omvdco2  18589  psgnunilem1  18634  pf1mpf  21017  pf1ind  21020  wilthlem3  25699  hoico1  29583  fmptco1f1o  30436  fcobijfs  30529  cycpmconjslem2  30896  cycpmconjs  30897  cyc3conja  30898  reprpmtf1o  32073  ltrncoidN  37575  trlcoabs2N  38169  trlcoat  38170  cdlemg47a  38181  cdlemg46  38182  trljco  38187  tendo1mulr  38218  tendo0co2  38235  cdlemi2  38266  cdlemk2  38279  cdlemk4  38281  cdlemk8  38285  cdlemk53  38404  cdlemk55a  38406  dvhopN  38563  dihopelvalcpre  38695  dihmeetlem1N  38737  dihglblem5apreN  38738  diophrw  39871  mendring  40307  rngccatidALTV  44781  ringccatidALTV  44844
 Copyright terms: Public domain W3C validator