Theorem fcoi2 6757

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 6542	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6250	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6641	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6265	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 18	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2817	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 220	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3895   I cid 5544  ran crn 5651   ↾ cres 5652   ∘ ccom 5654  Rel wrel 5655   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  fcof1oinvd  7301  mapen  9163  mapfien  9403  hashfacen  14602  cofulid  18070  setccatid  18264  estrccatid  18311  efmndid  19089  efmndmnd  19090  symggrp  19619  f1omvdco2  19667  symggen  19689  psgnunilem1  19712  gsumval3  20126  gsumzf1o  20131  frgpcyg  21884  f1linds  22136  qtophmeo  24141  motgrp  29011  hoico2  32364  fcoinver  33245  fcobij  33358  fcobijfs2  33360  symgfcoeu  33689  symgcom  33690  pmtrcnel2  33697  cycpmconjs  33763  subfacp1lem5  36035  ltrncoidN  41278  trlcoat  41873  trlcone  41878  cdlemg47a  41884  cdlemg47  41886  trljco  41890  tgrpgrplem  41899  tendo1mul  41920  tendo0pl  41941  cdlemkid2  42074  cdlemk45  42097  cdlemk53b  42106  erng1r  42145  tendocnv  42171  dvalveclem  42175  dva0g  42177  dvhgrp  42257  dvhlveclem  42258  dvh0g  42261  cdlemn8  42354  dihordlem7b  42365  dihopelvalcpre  42398  aks6d1c6lem5  43320  mendring  44283  rngccatidALTV  49462  ringccatidALTV  49496  cofu1stfix  50305