Theorem fcoi2 6760

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3908   I cid 5560  ran crn 5667   ↾ cres 5668   ∘ ccom 5670  Rel wrel 5671   Fn wfn 6538  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  fcof1oinvd  7302  mapen  9139  mapfien  9378  hashfacen  14511  cofulid  17972  setccatid  18166  estrccatid  18213  efmndid  18978  efmndmnd  18979  symggrp  19501  f1omvdco2  19549  symggen  19571  psgnunilem1  19594  gsumval3  20008  gsumzf1o  20013  frgpcyg  21760  f1linds  22012  qtophmeo  24011  motgrp  28849  hoico2  32146  fcoinver  32986  fcobij  33102  fcobijfs2  33104  symgfcoeu  33433  symgcom  33434  pmtrcnel2  33441  cycpmconjs  33507  subfacp1lem5  35697  ltrncoidN  40943  trlcoat  41538  trlcone  41543  cdlemg47a  41549  cdlemg47  41551  trljco  41555  tgrpgrplem  41564  tendo1mul  41585  tendo0pl  41606  cdlemkid2  41739  cdlemk45  41762  cdlemk53b  41771  erng1r  41810  tendocnv  41836  dvalveclem  41840  dva0g  41842  dvhgrp  41922  dvhlveclem  41923  dvh0g  41926  cdlemn8  42019  dihordlem7b  42030  dihopelvalcpre  42063  aks6d1c6lem5  42985  mendring  43956  rngccatidALTV  49078  ringccatidALTV  49112