Theorem fcoi2 6686

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ⊆ wss 3896   I cid 5505  ran crn 5608   ↾ cres 5609   ∘ ccom 5611  Rel wrel 5612   Fn wfn 6460  ⟶wf 6461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5087  df-opab 5149  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-fun 6467  df-fn 6468  df-f 6469

This theorem is referenced by:  fcof1oinvd  7204  mapen  8984  mapfien  9243  hashfacen  14244  hashfacenOLD  14245  cofulid  17679  setccatid  17873  estrccatid  17922  efmndid  18600  efmndmnd  18601  symggrp  19081  f1omvdco2  19129  symggen  19151  psgnunilem1  19174  gsumval3  19580  gsumzf1o  19585  frgpcyg  20861  f1linds  21112  qtophmeo  23048  motgrp  27037  hoico2  30251  fcoinver  31077  fcobij  31188  symgfcoeu  31482  symgcom  31483  pmtrcnel2  31490  cycpmconjs  31554  subfacp1lem5  33281  ltrncoidN  38368  trlcoat  38963  trlcone  38968  cdlemg47a  38974  cdlemg47  38976  trljco  38980  tgrpgrplem  38989  tendo1mul  39010  tendo0pl  39031  cdlemkid2  39164  cdlemk45  39187  cdlemk53b  39196  erng1r  39235  tendocnv  39261  dvalveclem  39265  dva0g  39267  dvhgrp  39347  dvhlveclem  39348  dvh0g  39351  cdlemn8  39444  dihordlem7b  39455  dihopelvalcpre  39488  mendring  41239  rngccatidALTV  45817  ringccatidALTV  45880