Theorem fcoi2 6553

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 6359	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6102	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6454	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6116	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2878	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 219	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3936   I cid 5459  ran crn 5556   ↾ cres 5557   ∘ ccom 5559  Rel wrel 5560   Fn wfn 6350  ⟶wf 6351

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-fun 6357  df-fn 6358  df-f 6359

This theorem is referenced by:  fcof1oinvd  7049  mapen  8681  mapfien  8871  hashfacen  13813  cofulid  17160  setccatid  17344  estrccatid  17382  efmndid  18053  efmndmnd  18054  symggrp  18528  f1omvdco2  18576  symggen  18598  psgnunilem1  18621  gsumval3  19027  gsumzf1o  19032  frgpcyg  20720  f1linds  20969  qtophmeo  22425  motgrp  26329  hoico2  29534  fcoinver  30357  fcobij  30458  symgfcoeu  30726  symgcom  30727  pmtrcnel2  30734  cycpmconjs  30798  subfacp1lem5  32431  ltrncoidN  37279  trlcoat  37874  trlcone  37879  cdlemg47a  37885  cdlemg47  37887  trljco  37891  tgrpgrplem  37900  tendo1mul  37921  tendo0pl  37942  cdlemkid2  38075  cdlemk45  38098  cdlemk53b  38107  erng1r  38146  tendocnv  38172  dvalveclem  38176  dva0g  38178  dvhgrp  38258  dvhlveclem  38259  dvh0g  38262  cdlemn8  38355  dihordlem7b  38366  dihopelvalcpre  38399  mendring  39812  rngccatidALTV  44280  ringccatidALTV  44343