Theorem fcoi2 6555

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 6361	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6104	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6456	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6118	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2880	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 219	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3938   I cid 5461  ran crn 5558   ↾ cres 5559   ∘ ccom 5561  Rel wrel 5562   Fn wfn 6352  ⟶wf 6353

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  fcof1oinvd  7051  mapen  8683  mapfien  8873  hashfacen  13815  cofulid  17162  setccatid  17346  estrccatid  17384  efmndid  18055  efmndmnd  18056  symggrp  18530  f1omvdco2  18578  symggen  18600  psgnunilem1  18623  gsumval3  19029  gsumzf1o  19034  frgpcyg  20722  f1linds  20971  qtophmeo  22427  motgrp  26331  hoico2  29536  fcoinver  30359  fcobij  30460  symgfcoeu  30728  symgcom  30729  pmtrcnel2  30736  cycpmconjs  30800  subfacp1lem5  32433  ltrncoidN  37266  trlcoat  37861  trlcone  37866  cdlemg47a  37872  cdlemg47  37874  trljco  37878  tgrpgrplem  37887  tendo1mul  37908  tendo0pl  37929  cdlemkid2  38062  cdlemk45  38085  cdlemk53b  38094  erng1r  38133  tendocnv  38159  dvalveclem  38163  dva0g  38165  dvhgrp  38245  dvhlveclem  38246  dvh0g  38249  cdlemn8  38342  dihordlem7b  38353  dihopelvalcpre  38386  mendring  39799  rngccatidALTV  44267  ringccatidALTV  44330