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

Theorem fcoi1 6423
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 6385 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 df-fn 6231 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eqimss 3946 . . . . 5 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
4 cnvi 5879 . . . . . . . . . 10 I = I
54reseq1i 5733 . . . . . . . . 9 ( I ↾ 𝐴) = ( I ↾ 𝐴)
65cnveqi 5634 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
7 cnvresid 6306 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
86, 7eqtr2i 2819 . . . . . . 7 ( I ↾ 𝐴) = ( I ↾ 𝐴)
98coeq2i 5620 . . . . . 6 (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹( I ↾ 𝐴))
10 cores2 5990 . . . . . 6 (dom 𝐹𝐴 → (𝐹( I ↾ 𝐴)) = (𝐹 ∘ I ))
119, 10syl5eq 2842 . . . . 5 (dom 𝐹𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
123, 11syl 17 . . . 4 (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13 funrel 6245 . . . . 5 (Fun 𝐹 → Rel 𝐹)
14 coi1 5993 . . . . 5 (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
1513, 14syl 17 . . . 4 (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
1612, 15sylan9eqr 2852 . . 3 ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
172, 16sylbi 218 . 2 (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
181, 17syl 17 1 (𝐹:𝐴𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wss 3861   I cid 5350  ccnv 5445  dom cdm 5446  cres 5448  ccom 5450  Rel wrel 5451  Fun wfun 6222   Fn wfn 6223  wf 6224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pr 5224
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-br 4965  df-opab 5027  df-id 5351  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-fun 6230  df-fn 6231  df-f 6232
This theorem is referenced by:  fcof1oinvd  6917  mapen  8531  mapfien  8720  hashfacen  13660  cofurid  16990  setccatid  17173  estrccatid  17211  curf2ndf  17326  symgid  18260  f1omvdco2  18307  psgnunilem1  18352  pf1mpf  20197  pf1ind  20200  wilthlem3  25329  hoico1  29216  fmptco1f1o  30060  fcobijfs  30139  cycpmconjslem2  30427  cycpmconjs  30428  cyc3conja  30429  reprpmtf1o  31506  ltrncoidN  36808  trlcoabs2N  37402  trlcoat  37403  cdlemg47a  37414  cdlemg46  37415  trljco  37420  tendo1mulr  37451  tendo0co2  37468  cdlemi2  37499  cdlemk2  37512  cdlemk4  37514  cdlemk8  37518  cdlemk53  37637  cdlemk55a  37639  dvhopN  37796  dihopelvalcpre  37928  dihmeetlem1N  37970  dihglblem5apreN  37971  diophrw  38854  mendring  39290  rngccatidALTV  43752  ringccatidALTV  43815
  Copyright terms: Public domain W3C validator