Theorem fcoi2 6782

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 6565	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6264	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6666	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6281	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 18	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2820	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 220	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900   I cid 5550  ran crn 5657   ↾ cres 5658   ∘ ccom 5660  Rel wrel 5661   Fn wfn 6556  ⟶wf 6557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-fun 6563  df-fn 6564  df-f 6565

This theorem is used by:  fcof1oinvd  7327  mapen  9191  mapfien  9430  hashfacen  14629  cofulid  18097  setccatid  18291  estrccatid  18338  efmndid  19116  efmndmnd  19117  symggrp  19647  f1omvdco2  19695  symggen  19717  psgnunilem1  19740  gsumval3  20154  gsumzf1o  20159  frgpcyg  21912  f1linds  22164  qtophmeo  24169  motgrp  29039  hoico2  32392  fcoinver  33273  fcobij  33385  fcobijfs2  33387  symgfcoeu  33719  symgcom  33720  pmtrcnel2  33727  cycpmconjs  33793  subfacp1lem5  36129  ltrncoidN  41388  trlcoat  41983  trlcone  41988  cdlemg47a  41994  cdlemg47  41996  trljco  42000  tgrpgrplem  42009  tendo1mul  42030  tendo0pl  42051  cdlemkid2  42184  cdlemk45  42207  cdlemk53b  42216  erng1r  42255  tendocnv  42281  dvalveclem  42285  dva0g  42287  dvhgrp  42367  dvhlveclem  42368  dvh0g  42371  cdlemn8  42464  dihordlem7b  42475  dihopelvalcpre  42508  aks6d1c6lem5  43430  mendring  44393  rngccatidALTV  49584  ringccatidALTV  49618  cofu1stfix  50427