# Metamath Proof Explorer

## Theorem cidval

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

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

### Proof

Step Hyp Ref Expression
1 cidfval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 cidfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 cidfval.o
4 cidfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 cidfval.i
6 cidval.x ${⊢}{\phi }\to {X}\in {B}$
7 1 2 3 4 5 cidfval
8 simpr ${⊢}\left({\phi }\wedge {x}={X}\right)\to {x}={X}$
9 8 8 oveq12d ${⊢}\left({\phi }\wedge {x}={X}\right)\to {x}{H}{x}={X}{H}{X}$
10 8 oveq2d ${⊢}\left({\phi }\wedge {x}={X}\right)\to {y}{H}{x}={y}{H}{X}$
11 8 opeq2d ${⊢}\left({\phi }\wedge {x}={X}\right)\to ⟨{y},{x}⟩=⟨{y},{X}⟩$
12 11 8 oveq12d
13 12 oveqd
14 13 eqeq1d
15 10 14 raleqbidv
16 8 oveq1d ${⊢}\left({\phi }\wedge {x}={X}\right)\to {x}{H}{y}={X}{H}{y}$
17 8 8 opeq12d ${⊢}\left({\phi }\wedge {x}={X}\right)\to ⟨{x},{x}⟩=⟨{X},{X}⟩$
18 17 oveq1d
19 18 oveqd
20 19 eqeq1d
21 16 20 raleqbidv
22 15 21 anbi12d
23 22 ralbidv
24 9 23 riotaeqbidv
25 riotaex
26 25 a1i
27 7 24 6 26 fvmptd