Theorem fcoi2 6738

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 6518	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6225	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6623	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6239	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2787	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 217	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3917   I cid 5535  ran crn 5642   ↾ cres 5643   ∘ ccom 5645  Rel wrel 5646   Fn wfn 6509  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  fcof1oinvd  7271  mapen  9111  mapfien  9366  hashfacen  14426  cofulid  17859  setccatid  18053  estrccatid  18100  efmndid  18822  efmndmnd  18823  symggrp  19337  f1omvdco2  19385  symggen  19407  psgnunilem1  19430  gsumval3  19844  gsumzf1o  19849  frgpcyg  21490  f1linds  21741  qtophmeo  23711  motgrp  28477  hoico2  31693  fcoinver  32540  fcobij  32652  symgfcoeu  33046  symgcom  33047  pmtrcnel2  33054  cycpmconjs  33120  subfacp1lem5  35178  ltrncoidN  40129  trlcoat  40724  trlcone  40729  cdlemg47a  40735  cdlemg47  40737  trljco  40741  tgrpgrplem  40750  tendo1mul  40771  tendo0pl  40792  cdlemkid2  40925  cdlemk45  40948  cdlemk53b  40957  erng1r  40996  tendocnv  41022  dvalveclem  41026  dva0g  41028  dvhgrp  41108  dvhlveclem  41109  dvh0g  41112  cdlemn8  41205  dihordlem7b  41216  dihopelvalcpre  41249  aks6d1c6lem5  42172  mendring  43184  rngccatidALTV  48264  ringccatidALTV  48298