# Metamath Proof Explorer

## Theorem catlid

Description: Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidcl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
catidcl.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
catidcl.i
catidcl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
catidcl.x ${⊢}{\phi }\to {X}\in {B}$
catlid.o
catlid.y ${⊢}{\phi }\to {Y}\in {B}$
catlid.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
Assertion catlid

### Proof

Step Hyp Ref Expression
1 catidcl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 catidcl.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 catidcl.i
4 catidcl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 catidcl.x ${⊢}{\phi }\to {X}\in {B}$
6 catlid.o
7 catlid.y ${⊢}{\phi }\to {Y}\in {B}$
8 catlid.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
9 oveq2
10 id ${⊢}{f}={F}\to {f}={F}$
11 9 10 eqeq12d
12 oveq1 ${⊢}{x}={X}\to {x}{H}{Y}={X}{H}{Y}$
13 opeq1 ${⊢}{x}={X}\to ⟨{x},{Y}⟩=⟨{X},{Y}⟩$
14 13 oveq1d
15 14 oveqd
16 15 eqeq1d
17 12 16 raleqbidv
18 simpl
19 18 ralimi
20 19 a1i
21 20 ss2rabi
22 1 2 6 4 3 7 cidval
23 1 2 6 4 7 catideu
24 riotacl2
25 23 24 syl
26 22 25 eqeltrd
27 21 26 sseldi
28 oveq1
29 28 eqeq1d
30 29 2ralbidv
31 30 elrab
32 31 simprbi
33 27 32 syl
34 17 33 5 rspcdva
35 11 34 8 rspcdva