Theorem fcoi2 6754

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 6541	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6249	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6638	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6264	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 18	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2819	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 220	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3902   I cid 5553  ran crn 5660   ↾ cres 5661   ∘ ccom 5663  Rel wrel 5664   Fn wfn 6532  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  fcof1oinvd  7298  mapen  9143  mapfien  9382  hashfacen  14523  cofulid  17985  setccatid  18179  estrccatid  18226  efmndid  19003  efmndmnd  19004  symggrp  19533  f1omvdco2  19581  symggen  19603  psgnunilem1  19626  gsumval3  20040  gsumzf1o  20045  frgpcyg  21792  f1linds  22044  qtophmeo  24049  motgrp  28893  hoico2  32246  fcoinver  33085  fcobij  33199  fcobijfs2  33201  symgfcoeu  33530  symgcom  33531  pmtrcnel2  33538  cycpmconjs  33604  subfacp1lem5  35771  ltrncoidN  41009  trlcoat  41604  trlcone  41609  cdlemg47a  41615  cdlemg47  41617  trljco  41621  tgrpgrplem  41630  tendo1mul  41651  tendo0pl  41672  cdlemkid2  41805  cdlemk45  41828  cdlemk53b  41837  erng1r  41876  tendocnv  41902  dvalveclem  41906  dva0g  41908  dvhgrp  41988  dvhlveclem  41989  dvh0g  41992  cdlemn8  42085  dihordlem7b  42096  dihopelvalcpre  42129  aks6d1c6lem5  43051  mendring  44037  rngccatidALTV  49195  ringccatidALTV  49229