Theorem fcoi2 6743

Description: Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
fcoi2	⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Proof of Theorem fcoi2

Step	Hyp	Ref	Expression
1		df-f 6529	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6239	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6627	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6254	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 18	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2822	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 220	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ⊆ wss 3907   I cid 5545  ran crn 5652   ↾ cres 5653   ∘ ccom 5655  Rel wrel 5656   Fn wfn 6520  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  fcof1oinvd  7281  mapen  9117  mapfien  9356  hashfacen  14479  cofulid  17935  setccatid  18129  estrccatid  18176  efmndid  18935  efmndmnd  18936  symggrp  19458  f1omvdco2  19506  symggen  19528  psgnunilem1  19551  gsumval3  19965  gsumzf1o  19970  frgpcyg  21680  f1linds  21932  qtophmeo  23931  motgrp  28766  hoico2  32014  fcoinver  32855  fcobij  32973  fcobijfs2  32975  symgfcoeu  33310  symgcom  33311  pmtrcnel2  33318  cycpmconjs  33384  subfacp1lem5  35542  ltrncoidN  40759  trlcoat  41354  trlcone  41359  cdlemg47a  41365  cdlemg47  41367  trljco  41371  tgrpgrplem  41380  tendo1mul  41401  tendo0pl  41422  cdlemkid2  41555  cdlemk45  41578  cdlemk53b  41587  erng1r  41626  tendocnv  41652  dvalveclem  41656  dva0g  41658  dvhgrp  41738  dvhlveclem  41739  dvh0g  41742  cdlemn8  41835  dihordlem7b  41846  dihopelvalcpre  41879  aks6d1c6lem5  42801  mendring  43772  rngccatidALTV  48893  ringccatidALTV  48927