Theorem fcoi2 6717

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 6504	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6215	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6602	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6230	. . . 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 3903   I cid 5526  ran crn 5633   ↾ cres 5634   ∘ ccom 5636  Rel wrel 5637   Fn wfn 6495  ⟶wf 6496

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fcof1oinvd  7249  mapen  9081  mapfien  9323  hashfacen  14389  cofulid  17826  setccatid  18020  estrccatid  18067  efmndid  18825  efmndmnd  18826  symggrp  19341  f1omvdco2  19389  symggen  19411  psgnunilem1  19434  gsumval3  19848  gsumzf1o  19853  frgpcyg  21540  f1linds  21792  qtophmeo  23773  motgrp  28627  hoico2  31844  fcoinver  32690  fcobij  32809  fcobijfs2  32811  symgfcoeu  33175  symgcom  33176  pmtrcnel2  33183  cycpmconjs  33249  subfacp1lem5  35397  ltrncoidN  40501  trlcoat  41096  trlcone  41101  cdlemg47a  41107  cdlemg47  41109  trljco  41113  tgrpgrplem  41122  tendo1mul  41143  tendo0pl  41164  cdlemkid2  41297  cdlemk45  41320  cdlemk53b  41329  erng1r  41368  tendocnv  41394  dvalveclem  41398  dva0g  41400  dvhgrp  41480  dvhlveclem  41481  dvh0g  41484  cdlemn8  41577  dihordlem7b  41588  dihopelvalcpre  41621  aks6d1c6lem5  42544  mendring  43542  rngccatidALTV  48629  ringccatidALTV  48663