![]() |
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 6715 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | df-fn 6544 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
3 | eqimss 4040 | . . . . 5 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | cnvi 6139 | . . . . . . . . . 10 ⊢ ◡ I = I | |
5 | 4 | reseq1i 5976 | . . . . . . . . 9 ⊢ (◡ I ↾ 𝐴) = ( I ↾ 𝐴) |
6 | 5 | cnveqi 5873 | . . . . . . . 8 ⊢ ◡(◡ I ↾ 𝐴) = ◡( I ↾ 𝐴) |
7 | cnvresid 6625 | . . . . . . . 8 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
8 | 6, 7 | eqtr2i 2762 | . . . . . . 7 ⊢ ( I ↾ 𝐴) = ◡(◡ I ↾ 𝐴) |
9 | 8 | coeq2i 5859 | . . . . . 6 ⊢ (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ ◡(◡ I ↾ 𝐴)) |
10 | cores2 6256 | . . . . . 6 ⊢ (dom 𝐹 ⊆ 𝐴 → (𝐹 ∘ ◡(◡ I ↾ 𝐴)) = (𝐹 ∘ I )) | |
11 | 9, 10 | eqtrid 2785 | . . . . 5 ⊢ (dom 𝐹 ⊆ 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I )) |
12 | 3, 11 | syl 17 | . . . 4 ⊢ (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I )) |
13 | funrel 6563 | . . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹) | |
14 | coi1 6259 | . . . . 5 ⊢ (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹) | |
15 | 13, 14 | syl 17 | . . . 4 ⊢ (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹) |
16 | 12, 15 | sylan9eqr 2795 | . . 3 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
17 | 2, 16 | sylbi 216 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
18 | 1, 17 | syl 17 | 1 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ⊆ wss 3948 I cid 5573 ◡ccnv 5675 dom cdm 5676 ↾ cres 5678 ∘ ccom 5680 Rel wrel 5681 Fun wfun 6535 Fn wfn 6536 ⟶wf 6537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-fun 6543 df-fn 6544 df-f 6545 |
This theorem is referenced by: fcof1oinvd 7288 mapen 9138 mapfien 9400 hashfacen 14410 hashfacenOLD 14411 cofurid 17838 setccatid 18031 estrccatid 18080 curf2ndf 18197 efmndid 18766 efmndmnd 18767 f1omvdco2 19311 psgnunilem1 19356 pf1mpf 21863 pf1ind 21866 wilthlem3 26564 hoico1 30997 fmptco1f1o 31845 fcobijfs 31936 cycpmconjslem2 32302 cycpmconjs 32303 cyc3conja 32304 reprpmtf1o 33627 ltrncoidN 38988 trlcoabs2N 39582 trlcoat 39583 cdlemg47a 39594 cdlemg46 39595 trljco 39600 tendo1mulr 39631 tendo0co2 39648 cdlemi2 39679 cdlemk2 39692 cdlemk4 39694 cdlemk8 39698 cdlemk53 39817 cdlemk55a 39819 dvhopN 39976 dihopelvalcpre 40108 dihmeetlem1N 40150 dihglblem5apreN 40151 diophrw 41483 mendring 41920 rngccatidALTV 46841 ringccatidALTV 46904 |
Copyright terms: Public domain | W3C validator |