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  18972  efmndmnd  18973  symggrp  19495  f1omvdco2  19543  symggen  19565  psgnunilem1  19588  gsumval3  20002  gsumzf1o  20007  frgpcyg  21753  f1linds  22005  qtophmeo  24004  motgrp  28842  hoico2  32139  fcoinver  32979  fcobij  33095  fcobijfs2  33097  symgfcoeu  33426  symgcom  33427  pmtrcnel2  33434  cycpmconjs  33500  subfacp1lem5  35689  ltrncoidN  40935  trlcoat  41530  trlcone  41535  cdlemg47a  41541  cdlemg47  41543  trljco  41547  tgrpgrplem  41556  tendo1mul  41577  tendo0pl  41598  cdlemkid2  41731  cdlemk45  41754  cdlemk53b  41763  erng1r  41802  tendocnv  41828  dvalveclem  41832  dva0g  41834  dvhgrp  41914  dvhlveclem  41915  dvh0g  41918  cdlemn8  42011  dihordlem7b  42022  dihopelvalcpre  42055  aks6d1c6lem5  42977  mendring  43948  rngccatidALTV  49070  ringccatidALTV  49104