![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > arwrid | Structured version Visualization version GIF version |
Description: Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ref | Expression |
---|---|
arwlid.h | ⊢ 𝐻 = (Homa‘𝐶) |
arwlid.o | ⊢ · = (compa‘𝐶) |
arwlid.a | ⊢ 1 = (Ida‘𝐶) |
arwlid.f | ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
Ref | Expression |
---|---|
arwrid | ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | arwlid.a | . . . . . 6 ⊢ 1 = (Ida‘𝐶) | |
2 | eqid 2771 | . . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶) | |
3 | arwlid.f | . . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) | |
4 | arwlid.h | . . . . . . . 8 ⊢ 𝐻 = (Homa‘𝐶) | |
5 | 4 | homarcl 17158 | . . . . . . 7 ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐶 ∈ Cat) |
6 | 3, 5 | syl 17 | . . . . . 6 ⊢ (𝜑 → 𝐶 ∈ Cat) |
7 | eqid 2771 | . . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶) | |
8 | 4, 2 | homarcl2 17165 | . . . . . . . 8 ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶))) |
9 | 3, 8 | syl 17 | . . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ (Base‘𝐶) ∧ 𝑌 ∈ (Base‘𝐶))) |
10 | 9 | simpld 487 | . . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) |
11 | 1, 2, 6, 7, 10 | ida2 17189 | . . . . 5 ⊢ (𝜑 → (2nd ‘( 1 ‘𝑋)) = ((Id‘𝐶)‘𝑋)) |
12 | 11 | oveq2d 6990 | . . . 4 ⊢ (𝜑 → ((2nd ‘𝐹)(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(2nd ‘( 1 ‘𝑋))) = ((2nd ‘𝐹)(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋))) |
13 | eqid 2771 | . . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶) | |
14 | eqid 2771 | . . . . 5 ⊢ (comp‘𝐶) = (comp‘𝐶) | |
15 | 9 | simprd 488 | . . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶)) |
16 | 4, 13 | homahom 17169 | . . . . . 6 ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → (2nd ‘𝐹) ∈ (𝑋(Hom ‘𝐶)𝑌)) |
17 | 3, 16 | syl 17 | . . . . 5 ⊢ (𝜑 → (2nd ‘𝐹) ∈ (𝑋(Hom ‘𝐶)𝑌)) |
18 | 2, 13, 7, 6, 10, 14, 15, 17 | catrid 16825 | . . . 4 ⊢ (𝜑 → ((2nd ‘𝐹)(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (2nd ‘𝐹)) |
19 | 12, 18 | eqtrd 2807 | . . 3 ⊢ (𝜑 → ((2nd ‘𝐹)(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(2nd ‘( 1 ‘𝑋))) = (2nd ‘𝐹)) |
20 | 19 | oteq3d 4687 | . 2 ⊢ (𝜑 → 〈𝑋, 𝑌, ((2nd ‘𝐹)(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(2nd ‘( 1 ‘𝑋)))〉 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) |
21 | arwlid.o | . . 3 ⊢ · = (compa‘𝐶) | |
22 | 1, 2, 6, 10, 4 | idahom 17190 | . . 3 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐻𝑋)) |
23 | 21, 4, 22, 3, 14 | coaval 17198 | . 2 ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 〈𝑋, 𝑌, ((2nd ‘𝐹)(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)(2nd ‘( 1 ‘𝑋)))〉) |
24 | 4 | homadmcd 17172 | . . 3 ⊢ (𝐹 ∈ (𝑋𝐻𝑌) → 𝐹 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) |
25 | 3, 24 | syl 17 | . 2 ⊢ (𝜑 → 𝐹 = 〈𝑋, 𝑌, (2nd ‘𝐹)〉) |
26 | 20, 23, 25 | 3eqtr4d 2817 | 1 ⊢ (𝜑 → (𝐹 · ( 1 ‘𝑋)) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1508 ∈ wcel 2051 〈cop 4441 〈cotp 4443 ‘cfv 6185 (class class class)co 6974 2nd c2nd 7498 Basecbs 16337 Hom chom 16430 compcco 16431 Catccat 16805 Idccid 16806 Homachoma 17153 Idacida 17183 compaccoa 17184 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-rep 5045 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-reu 3088 df-rmo 3089 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-ot 4444 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-1st 7499 df-2nd 7500 df-cat 16809 df-cid 16810 df-doma 17154 df-coda 17155 df-homa 17156 df-arw 17157 df-ida 17185 df-coa 17186 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |