Theorem fcoi2 6709

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 6496	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6207	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6594	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6222	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2794	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 217	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3890   I cid 5518  ran crn 5625   ↾ cres 5626   ∘ ccom 5628  Rel wrel 5629   Fn wfn 6487  ⟶wf 6488

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fcof1oinvd  7241  mapen  9072  mapfien  9314  hashfacen  14407  cofulid  17848  setccatid  18042  estrccatid  18089  efmndid  18847  efmndmnd  18848  symggrp  19366  f1omvdco2  19414  symggen  19436  psgnunilem1  19459  gsumval3  19873  gsumzf1o  19878  frgpcyg  21563  f1linds  21815  qtophmeo  23792  motgrp  28625  hoico2  31843  fcoinver  32689  fcobij  32808  fcobijfs2  32810  symgfcoeu  33158  symgcom  33159  pmtrcnel2  33166  cycpmconjs  33232  subfacp1lem5  35382  ltrncoidN  40588  trlcoat  41183  trlcone  41188  cdlemg47a  41194  cdlemg47  41196  trljco  41200  tgrpgrplem  41209  tendo1mul  41230  tendo0pl  41251  cdlemkid2  41384  cdlemk45  41407  cdlemk53b  41416  erng1r  41455  tendocnv  41481  dvalveclem  41485  dva0g  41487  dvhgrp  41567  dvhlveclem  41568  dvh0g  41571  cdlemn8  41664  dihordlem7b  41675  dihopelvalcpre  41708  aks6d1c6lem5  42630  mendring  43634  rngccatidALTV  48760  ringccatidALTV  48794