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

Theorem arwlid 14217
 Description: Left 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
arwlid

Proof of Theorem arwlid
StepHypRef Expression
1 arwlid.a . . . . . 6 Ida
2 eqid 2435 . . . . . 6
3 arwlid.f . . . . . . 7
4 arwlid.h . . . . . . . 8 Homa
54homarcl 14173 . . . . . . 7
63, 5syl 16 . . . . . 6
7 eqid 2435 . . . . . 6
84, 2homarcl2 14180 . . . . . . . 8
93, 8syl 16 . . . . . . 7
109simprd 450 . . . . . 6
111, 2, 6, 7, 10ida2 14204 . . . . 5
1211oveq1d 6088 . . . 4 comp comp
13 eqid 2435 . . . . 5
149simpld 446 . . . . 5
15 eqid 2435 . . . . 5 comp comp
164, 13homahom 14184 . . . . . 6
173, 16syl 16 . . . . 5
182, 13, 7, 6, 14, 15, 10, 17catlid 13898 . . . 4 comp
1912, 18eqtrd 2467 . . 3 comp
2019oteq3d 3990 . 2 comp
21 arwlid.o . . 3 compa
221, 2, 6, 10, 4idahom 14205 . . 3
2321, 4, 3, 22, 15coaval 14213 . 2 comp