Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  arwrid Structured version   Unicode version

Theorem arwrid 14220
 Description: Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
arwlid.h Homa
arwlid.o compa
arwlid.a Ida
arwlid.f
Assertion
Ref Expression
arwrid

Proof of Theorem arwrid
StepHypRef Expression
1 arwlid.a . . . . . 6 Ida
2 eqid 2435 . . . . . 6
3 arwlid.f . . . . . . 7
4 arwlid.h . . . . . . . 8 Homa
54homarcl 14175 . . . . . . 7
63, 5syl 16 . . . . . 6
7 eqid 2435 . . . . . 6
84, 2homarcl2 14182 . . . . . . . 8
93, 8syl 16 . . . . . . 7
109simpld 446 . . . . . 6
111, 2, 6, 7, 10ida2 14206 . . . . 5
1211oveq2d 6089 . . . 4 comp comp
13 eqid 2435 . . . . 5
14 eqid 2435 . . . . 5 comp comp
159simprd 450 . . . . 5
164, 13homahom 14186 . . . . . 6
173, 16syl 16 . . . . 5
182, 13, 7, 6, 10, 14, 15, 17catrid 13901 . . . 4 comp
1912, 18eqtrd 2467 . . 3 comp
2019oteq3d 3990 . 2 comp
21 arwlid.o . . 3 compa
221, 2, 6, 10, 4idahom 14207 . . 3
2321, 4, 22, 3, 14coaval 14215 . 2 comp