# Metamath Proof Explorer

## Theorem catidex

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

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

### Proof

Step Hyp Ref Expression
1 catidex.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 catidex.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 catidex.o
4 catidex.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 catidex.x ${⊢}{\phi }\to {X}\in {B}$
6 id ${⊢}{x}={X}\to {x}={X}$
7 6 6 oveq12d ${⊢}{x}={X}\to {x}{H}{x}={X}{H}{X}$
8 oveq2 ${⊢}{x}={X}\to {y}{H}{x}={y}{H}{X}$
9 opeq2 ${⊢}{x}={X}\to ⟨{y},{x}⟩=⟨{y},{X}⟩$
10 9 6 oveq12d
11 10 oveqd
12 11 eqeq1d
13 8 12 raleqbidv
14 oveq1 ${⊢}{x}={X}\to {x}{H}{y}={X}{H}{y}$
15 6 6 opeq12d ${⊢}{x}={X}\to ⟨{x},{x}⟩=⟨{X},{X}⟩$
16 15 oveq1d
17 16 oveqd
18 17 eqeq1d
19 14 18 raleqbidv
20 13 19 anbi12d
21 20 ralbidv
22 7 21 rexeqbidv
23 1 2 3 iscat
24 23 ibi
25 simpl
26 25 ralimi
27 4 24 26 3syl
28 22 27 5 rspcdva