Theorem fcoi2 6329

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 6139	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 5892	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6234	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 5906	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2836	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 209	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ⊆ wss 3792   I cid 5260  ran crn 5356   ↾ cres 5357   ∘ ccom 5359  Rel wrel 5360   Fn wfn 6130  ⟶wf 6131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-fun 6137  df-fn 6138  df-f 6139

This theorem is referenced by:  fcof1oinvd  6820  mapen  8412  mapfien  8601  hashfacen  13552  cofulid  16935  setccatid  17119  estrccatid  17157  symggrp  18203  f1omvdco2  18251  symggen  18273  psgnunilem1  18296  gsumval3  18694  gsumzf1o  18699  frgpcyg  20317  f1linds  20568  qtophmeo  22029  motgrp  25894  hoico2  29188  fcoinver  29981  fcobij  30066  symgfcoeu  30443  subfacp1lem5  31765  ltrncoidN  36282  trlcoat  36877  trlcone  36882  cdlemg47a  36888  cdlemg47  36890  trljco  36894  tgrpgrplem  36903  tendo1mul  36924  tendo0pl  36945  cdlemkid2  37078  cdlemk45  37101  cdlemk53b  37110  erng1r  37149  tendocnv  37175  dvalveclem  37179  dva0g  37181  dvhgrp  37261  dvhlveclem  37262  dvh0g  37265  cdlemn8  37358  dihordlem7b  37369  dihopelvalcpre  37402  mendring  38721  rngccatidALTV  43004  ringccatidALTV  43067