# Metamath Proof Explorer

## Theorem cidfval

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-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
Assertion cidfval

### 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 fvexd ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}\in \mathrm{V}$
7 fveq2 ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}={\mathrm{Base}}_{{C}}$
8 7 1 syl6eqr ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}={B}$
9 fvexd ${⊢}\left({c}={C}\wedge {b}={B}\right)\to \mathrm{Hom}\left({c}\right)\in \mathrm{V}$
10 simpl ${⊢}\left({c}={C}\wedge {b}={B}\right)\to {c}={C}$
11 10 fveq2d ${⊢}\left({c}={C}\wedge {b}={B}\right)\to \mathrm{Hom}\left({c}\right)=\mathrm{Hom}\left({C}\right)$
12 11 2 syl6eqr ${⊢}\left({c}={C}\wedge {b}={B}\right)\to \mathrm{Hom}\left({c}\right)={H}$
13 fvexd ${⊢}\left(\left({c}={C}\wedge {b}={B}\right)\wedge {h}={H}\right)\to \mathrm{comp}\left({c}\right)\in \mathrm{V}$
14 simpll ${⊢}\left(\left({c}={C}\wedge {b}={B}\right)\wedge {h}={H}\right)\to {c}={C}$
15 14 fveq2d ${⊢}\left(\left({c}={C}\wedge {b}={B}\right)\wedge {h}={H}\right)\to \mathrm{comp}\left({c}\right)=\mathrm{comp}\left({C}\right)$
16 15 3 syl6eqr
17 simpllr
18 simplr
19 18 oveqd
20 18 oveqd
21 simpr
22 21 oveqd
23 22 oveqd
24 23 eqeq1d
25 20 24 raleqbidv
26 18 oveqd
27 21 oveqd
28 27 oveqd
29 28 eqeq1d
30 26 29 raleqbidv
31 25 30 anbi12d
32 17 31 raleqbidv
33 19 32 riotaeqbidv
34 17 33 mpteq12dv
35 13 16 34 csbied2
36 9 12 35 csbied2
37 6 8 36 csbied2
38 df-cid
39 37 38 1 mptfvmpt
40 4 39 syl
41 5 40 syl5eq