Theorem fcoi2 6709

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3890   I cid 5519  ran crn 5626   ↾ cres 5627   ∘ ccom 5629  Rel wrel 5630   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fcof1oinvd  7244  mapen  9076  mapfien  9318  hashfacen  14414  cofulid  17855  setccatid  18049  estrccatid  18096  efmndid  18854  efmndmnd  18855  symggrp  19373  f1omvdco2  19421  symggen  19443  psgnunilem1  19466  gsumval3  19880  gsumzf1o  19885  frgpcyg  21555  f1linds  21807  qtophmeo  23807  motgrp  28636  hoico2  31853  fcoinver  32700  fcobij  32819  fcobijfs2  32821  symgfcoeu  33170  symgcom  33171  pmtrcnel2  33178  cycpmconjs  33244  subfacp1lem5  35419  ltrncoidN  40627  trlcoat  41222  trlcone  41227  cdlemg47a  41233  cdlemg47  41235  trljco  41239  tgrpgrplem  41248  tendo1mul  41269  tendo0pl  41290  cdlemkid2  41423  cdlemk45  41446  cdlemk53b  41455  erng1r  41494  tendocnv  41520  dvalveclem  41524  dva0g  41526  dvhgrp  41606  dvhlveclem  41607  dvh0g  41610  cdlemn8  41703  dihordlem7b  41714  dihopelvalcpre  41747  aks6d1c6lem5  42669  mendring  43640  rngccatidALTV  48770  ringccatidALTV  48804