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

Theorem fcoi1 6717
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 6669 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 df-fn 6500 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eqimss 4001 . . . . 5 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
4 cnvi 6095 . . . . . . . . . 10 I = I
54reseq1i 5934 . . . . . . . . 9 ( I ↾ 𝐴) = ( I ↾ 𝐴)
65cnveqi 5831 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
7 cnvresid 6581 . . . . . . . 8 ( I ↾ 𝐴) = ( I ↾ 𝐴)
86, 7eqtr2i 2766 . . . . . . 7 ( I ↾ 𝐴) = ( I ↾ 𝐴)
98coeq2i 5817 . . . . . 6 (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹( I ↾ 𝐴))
10 cores2 6212 . . . . . 6 (dom 𝐹𝐴 → (𝐹( I ↾ 𝐴)) = (𝐹 ∘ I ))
119, 10eqtrid 2789 . . . . 5 (dom 𝐹𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
123, 11syl 17 . . . 4 (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13 funrel 6519 . . . . 5 (Fun 𝐹 → Rel 𝐹)
14 coi1 6215 . . . . 5 (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
1513, 14syl 17 . . . 4 (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
1612, 15sylan9eqr 2799 . . 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 3911   I cid 5531  ccnv 5633  dom cdm 5634  cres 5636  ccom 5638  Rel wrel 5639  Fun wfun 6491   Fn wfn 6492  wf 6493
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 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  fcof1oinvd  7240  mapen  9086  mapfien  9345  hashfacen  14352  hashfacenOLD  14353  cofurid  17778  setccatid  17971  estrccatid  18020  curf2ndf  18137  efmndid  18699  efmndmnd  18700  f1omvdco2  19231  psgnunilem1  19276  pf1mpf  21721  pf1ind  21724  wilthlem3  26422  hoico1  30701  fmptco1f1o  31550  fcobijfs  31643  cycpmconjslem2  32007  cycpmconjs  32008  cyc3conja  32009  reprpmtf1o  33242  ltrncoidN  38594  trlcoabs2N  39188  trlcoat  39189  cdlemg47a  39200  cdlemg46  39201  trljco  39206  tendo1mulr  39237  tendo0co2  39254  cdlemi2  39285  cdlemk2  39298  cdlemk4  39300  cdlemk8  39304  cdlemk53  39423  cdlemk55a  39425  dvhopN  39582  dihopelvalcpre  39714  dihmeetlem1N  39756  dihglblem5apreN  39757  diophrw  41085  mendring  41522  rngccatidALTV  46294  ringccatidALTV  46357
  Copyright terms: Public domain W3C validator