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 2793	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 217	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3901   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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  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  7239  mapen  9069  mapfien  9311  hashfacen  14377  cofulid  17814  setccatid  18008  estrccatid  18055  efmndid  18813  efmndmnd  18814  symggrp  19329  f1omvdco2  19377  symggen  19399  psgnunilem1  19422  gsumval3  19836  gsumzf1o  19841  frgpcyg  21528  f1linds  21780  qtophmeo  23761  motgrp  28615  hoico2  31832  fcoinver  32679  fcobij  32799  fcobijfs2  32801  symgfcoeu  33164  symgcom  33165  pmtrcnel2  33172  cycpmconjs  33238  subfacp1lem5  35378  ltrncoidN  40388  trlcoat  40983  trlcone  40988  cdlemg47a  40994  cdlemg47  40996  trljco  41000  tgrpgrplem  41009  tendo1mul  41030  tendo0pl  41051  cdlemkid2  41184  cdlemk45  41207  cdlemk53b  41216  erng1r  41255  tendocnv  41281  dvalveclem  41285  dva0g  41287  dvhgrp  41367  dvhlveclem  41368  dvh0g  41371  cdlemn8  41464  dihordlem7b  41475  dihopelvalcpre  41508  aks6d1c6lem5  42431  mendring  43430  rngccatidALTV  48518  ringccatidALTV  48552