Theorem fcoi2 6783

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ⊆ wss 3962   I cid 5581  ran crn 5689   ↾ cres 5690   ∘ ccom 5692  Rel wrel 5693   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  fcof1oinvd  7312  mapen  9179  mapfien  9445  hashfacen  14489  cofulid  17940  setccatid  18137  estrccatid  18186  efmndid  18913  efmndmnd  18914  symggrp  19432  f1omvdco2  19480  symggen  19502  psgnunilem1  19525  gsumval3  19939  gsumzf1o  19944  frgpcyg  21609  f1linds  21862  qtophmeo  23840  motgrp  28565  hoico2  31785  fcoinver  32623  fcobij  32739  symgfcoeu  33084  symgcom  33085  pmtrcnel2  33092  cycpmconjs  33158  subfacp1lem5  35168  ltrncoidN  40110  trlcoat  40705  trlcone  40710  cdlemg47a  40716  cdlemg47  40718  trljco  40722  tgrpgrplem  40731  tendo1mul  40752  tendo0pl  40773  cdlemkid2  40906  cdlemk45  40929  cdlemk53b  40938  erng1r  40977  tendocnv  41003  dvalveclem  41007  dva0g  41009  dvhgrp  41089  dvhlveclem  41090  dvh0g  41093  cdlemn8  41186  dihordlem7b  41197  dihopelvalcpre  41230  aks6d1c6lem5  42158  mendring  43176  rngccatidALTV  48115  ringccatidALTV  48149