![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fcoi1 | Structured version Visualization version GIF version |
Description: Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fcoi1 | ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 6385 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | df-fn 6231 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
3 | eqimss 3946 | . . . . 5 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | cnvi 5879 | . . . . . . . . . 10 ⊢ ◡ I = I | |
5 | 4 | reseq1i 5733 | . . . . . . . . 9 ⊢ (◡ I ↾ 𝐴) = ( I ↾ 𝐴) |
6 | 5 | cnveqi 5634 | . . . . . . . 8 ⊢ ◡(◡ I ↾ 𝐴) = ◡( I ↾ 𝐴) |
7 | cnvresid 6306 | . . . . . . . 8 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
8 | 6, 7 | eqtr2i 2819 | . . . . . . 7 ⊢ ( I ↾ 𝐴) = ◡(◡ I ↾ 𝐴) |
9 | 8 | coeq2i 5620 | . . . . . 6 ⊢ (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ ◡(◡ I ↾ 𝐴)) |
10 | cores2 5990 | . . . . . 6 ⊢ (dom 𝐹 ⊆ 𝐴 → (𝐹 ∘ ◡(◡ I ↾ 𝐴)) = (𝐹 ∘ I )) | |
11 | 9, 10 | syl5eq 2842 | . . . . 5 ⊢ (dom 𝐹 ⊆ 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I )) |
12 | 3, 11 | syl 17 | . . . 4 ⊢ (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I )) |
13 | funrel 6245 | . . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹) | |
14 | coi1 5993 | . . . . 5 ⊢ (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹) | |
15 | 13, 14 | syl 17 | . . . 4 ⊢ (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹) |
16 | 12, 15 | sylan9eqr 2852 | . . 3 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
17 | 2, 16 | sylbi 218 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
18 | 1, 17 | syl 17 | 1 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ⊆ wss 3861 I cid 5350 ◡ccnv 5445 dom cdm 5446 ↾ cres 5448 ∘ ccom 5450 Rel wrel 5451 Fun wfun 6222 Fn wfn 6223 ⟶wf 6224 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pr 5224 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-op 4481 df-br 4965 df-opab 5027 df-id 5351 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-fun 6230 df-fn 6231 df-f 6232 |
This theorem is referenced by: fcof1oinvd 6917 mapen 8531 mapfien 8720 hashfacen 13660 cofurid 16990 setccatid 17173 estrccatid 17211 curf2ndf 17326 symgid 18260 f1omvdco2 18307 psgnunilem1 18352 pf1mpf 20197 pf1ind 20200 wilthlem3 25329 hoico1 29216 fmptco1f1o 30060 fcobijfs 30139 cycpmconjslem2 30427 cycpmconjs 30428 cyc3conja 30429 reprpmtf1o 31506 ltrncoidN 36808 trlcoabs2N 37402 trlcoat 37403 cdlemg47a 37414 cdlemg46 37415 trljco 37420 tendo1mulr 37451 tendo0co2 37468 cdlemi2 37499 cdlemk2 37512 cdlemk4 37514 cdlemk8 37518 cdlemk53 37637 cdlemk55a 37639 dvhopN 37796 dihopelvalcpre 37928 dihmeetlem1N 37970 dihglblem5apreN 37971 diophrw 38854 mendring 39290 rngccatidALTV 43752 ringccatidALTV 43815 |
Copyright terms: Public domain | W3C validator |