Theorem fcoi2 6735

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3914   I cid 5532  ran crn 5639   ↾ cres 5640   ∘ ccom 5642  Rel wrel 5643   Fn wfn 6506  ⟶wf 6507

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fcof1oinvd  7268  mapen  9105  mapfien  9359  hashfacen  14419  cofulid  17852  setccatid  18046  estrccatid  18093  efmndid  18815  efmndmnd  18816  symggrp  19330  f1omvdco2  19378  symggen  19400  psgnunilem1  19423  gsumval3  19837  gsumzf1o  19842  frgpcyg  21483  f1linds  21734  qtophmeo  23704  motgrp  28470  hoico2  31686  fcoinver  32533  fcobij  32645  symgfcoeu  33039  symgcom  33040  pmtrcnel2  33047  cycpmconjs  33113  subfacp1lem5  35171  ltrncoidN  40122  trlcoat  40717  trlcone  40722  cdlemg47a  40728  cdlemg47  40730  trljco  40734  tgrpgrplem  40743  tendo1mul  40764  tendo0pl  40785  cdlemkid2  40918  cdlemk45  40941  cdlemk53b  40950  erng1r  40989  tendocnv  41015  dvalveclem  41019  dva0g  41021  dvhgrp  41101  dvhlveclem  41102  dvh0g  41105  cdlemn8  41198  dihordlem7b  41209  dihopelvalcpre  41242  aks6d1c6lem5  42165  mendring  43177  rngccatidALTV  48260  ringccatidALTV  48294