Theorem fcoi2 6117

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 5930	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		cores 5676	. . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹))
3		fnrel 6027	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
4		coi2 5690	. . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹)
5	3, 4	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹)
6	2, 5	sylan9eqr 2707	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
7	1, 6	sylbi 207	1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ⊆ wss 3607   I cid 5052  ran crn 5144   ↾ cres 5145   ∘ ccom 5147  Rel wrel 5148   Fn wfn 5921  ⟶wf 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-fun 5928  df-fn 5929  df-f 5930

This theorem is referenced by:  fcof1oinvd  6588  mapen  8165  mapfien  8354  hashfacen  13276  cofulid  16597  setccatid  16781  estrccatid  16819  symggrp  17866  f1omvdco2  17914  symggen  17936  psgnunilem1  17959  gsumval3  18354  gsumzf1o  18359  frgpcyg  19970  f1linds  20212  qtophmeo  21668  motgrp  25483  hoico2  28744  fcoinver  29544  fcobij  29628  symgfcoeu  29973  subfacp1lem5  31292  ltrncoidN  35732  trlcoat  36328  trlcone  36333  cdlemg47a  36339  cdlemg47  36341  trljco  36345  tgrpgrplem  36354  tendo1mul  36375  tendo0pl  36396  cdlemkid2  36529  cdlemk45  36552  cdlemk53b  36561  erng1r  36600  tendocnv  36627  dvalveclem  36631  dva0g  36633  dvhgrp  36713  dvhlveclem  36714  dvh0g  36717  cdlemn8  36810  dihordlem7b  36821  dihopelvalcpre  36854  mendring  38079  rngccatidALTV  42314  ringccatidALTV  42377