Theorem fcoi2 6633

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 6422	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6142	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6519	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6156	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2801	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 216	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3883   I cid 5479  ran crn 5581   ↾ cres 5582   ∘ ccom 5584  Rel wrel 5585   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fcof1oinvd  7145  mapen  8877  mapfien  9097  hashfacen  14094  hashfacenOLD  14095  cofulid  17521  setccatid  17715  estrccatid  17764  efmndid  18442  efmndmnd  18443  symggrp  18923  f1omvdco2  18971  symggen  18993  psgnunilem1  19016  gsumval3  19423  gsumzf1o  19428  frgpcyg  20693  f1linds  20942  qtophmeo  22876  motgrp  26808  hoico2  30020  fcoinver  30847  fcobij  30959  symgfcoeu  31253  symgcom  31254  pmtrcnel2  31261  cycpmconjs  31325  subfacp1lem5  33046  ltrncoidN  38069  trlcoat  38664  trlcone  38669  cdlemg47a  38675  cdlemg47  38677  trljco  38681  tgrpgrplem  38690  tendo1mul  38711  tendo0pl  38732  cdlemkid2  38865  cdlemk45  38888  cdlemk53b  38897  erng1r  38936  tendocnv  38962  dvalveclem  38966  dva0g  38968  dvhgrp  39048  dvhlveclem  39049  dvh0g  39052  cdlemn8  39145  dihordlem7b  39156  dihopelvalcpre  39189  mendring  40933  rngccatidALTV  45435  ringccatidALTV  45498