![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fcoi2 | Structured version Visualization version GIF version |
Description: Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fcoi2 | ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 6139 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | cores 5892 | . . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = ( I ∘ 𝐹)) | |
3 | fnrel 6234 | . . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
4 | coi2 5906 | . . . 4 ⊢ (Rel 𝐹 → ( I ∘ 𝐹) = 𝐹) | |
5 | 3, 4 | syl 17 | . . 3 ⊢ (𝐹 Fn 𝐴 → ( I ∘ 𝐹) = 𝐹) |
6 | 2, 5 | sylan9eqr 2836 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹) |
7 | 1, 6 | sylbi 209 | 1 ⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ⊆ wss 3792 I cid 5260 ran crn 5356 ↾ cres 5357 ∘ ccom 5359 Rel wrel 5360 Fn wfn 6130 ⟶wf 6131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-opab 4949 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-fun 6137 df-fn 6138 df-f 6139 |
This theorem is referenced by: fcof1oinvd 6820 mapen 8412 mapfien 8601 hashfacen 13552 cofulid 16935 setccatid 17119 estrccatid 17157 symggrp 18203 f1omvdco2 18251 symggen 18273 psgnunilem1 18296 gsumval3 18694 gsumzf1o 18699 frgpcyg 20317 f1linds 20568 qtophmeo 22029 motgrp 25894 hoico2 29188 fcoinver 29981 fcobij 30066 symgfcoeu 30443 subfacp1lem5 31765 ltrncoidN 36282 trlcoat 36877 trlcone 36882 cdlemg47a 36888 cdlemg47 36890 trljco 36894 tgrpgrplem 36903 tendo1mul 36924 tendo0pl 36945 cdlemkid2 37078 cdlemk45 37101 cdlemk53b 37110 erng1r 37149 tendocnv 37175 dvalveclem 37179 dva0g 37181 dvhgrp 37261 dvhlveclem 37262 dvh0g 37265 cdlemn8 37358 dihordlem7b 37369 dihopelvalcpre 37402 mendring 38721 rngccatidALTV 43004 ringccatidALTV 43067 |
Copyright terms: Public domain | W3C validator |