Theorem fcoi2 6752

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3926   I cid 5547  ran crn 5655   ↾ cres 5656   ∘ ccom 5658  Rel wrel 5659   Fn wfn 6525  ⟶wf 6526

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  fcof1oinvd  7285  mapen  9153  mapfien  9418  hashfacen  14470  cofulid  17901  setccatid  18095  estrccatid  18142  efmndid  18864  efmndmnd  18865  symggrp  19379  f1omvdco2  19427  symggen  19449  psgnunilem1  19472  gsumval3  19886  gsumzf1o  19891  frgpcyg  21532  f1linds  21783  qtophmeo  23753  motgrp  28468  hoico2  31684  fcoinver  32531  fcobij  32645  symgfcoeu  33039  symgcom  33040  pmtrcnel2  33047  cycpmconjs  33113  subfacp1lem5  35152  ltrncoidN  40093  trlcoat  40688  trlcone  40693  cdlemg47a  40699  cdlemg47  40701  trljco  40705  tgrpgrplem  40714  tendo1mul  40735  tendo0pl  40756  cdlemkid2  40889  cdlemk45  40912  cdlemk53b  40921  erng1r  40960  tendocnv  40986  dvalveclem  40990  dva0g  40992  dvhgrp  41072  dvhlveclem  41073  dvh0g  41076  cdlemn8  41169  dihordlem7b  41180  dihopelvalcpre  41213  aks6d1c6lem5  42136  mendring  43159  rngccatidALTV  48195  ringccatidALTV  48229