Theorem fcoi2 6755

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 6542	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 6252	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6639	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 6267	. . . 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 ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ⊆ wss 3906   I cid 5557  ran crn 5664   ↾ cres 5665   ∘ ccom 5667  Rel wrel 5668   Fn wfn 6533  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  fcof1oinvd  7293  mapen  9130  mapfien  9369  hashfacen  14493  cofulid  17948  setccatid  18142  estrccatid  18189  efmndid  18948  efmndmnd  18949  symggrp  19471  f1omvdco2  19519  symggen  19541  psgnunilem1  19564  gsumval3  19978  gsumzf1o  19983  frgpcyg  21704  f1linds  21956  qtophmeo  23955  motgrp  28793  hoico2  32090  fcoinver  32930  fcobij  33046  fcobijfs2  33048  symgfcoeu  33383  symgcom  33384  pmtrcnel2  33391  cycpmconjs  33457  subfacp1lem5  35657  ltrncoidN  40883  trlcoat  41478  trlcone  41483  cdlemg47a  41489  cdlemg47  41491  trljco  41495  tgrpgrplem  41504  tendo1mul  41525  tendo0pl  41546  cdlemkid2  41679  cdlemk45  41702  cdlemk53b  41711  erng1r  41750  tendocnv  41776  dvalveclem  41780  dva0g  41782  dvhgrp  41862  dvhlveclem  41863  dvh0g  41866  cdlemn8  41959  dihordlem7b  41970  dihopelvalcpre  42003  aks6d1c6lem5  42925  mendring  43898  rngccatidALTV  49020  ringccatidALTV  49054