# Metamath Proof Explorer

## Theorem iscat

Description: The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses iscat.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
iscat.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
iscat.o
Assertion iscat

### Proof

Step Hyp Ref Expression
1 iscat.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 iscat.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 iscat.o
4 fvexd ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}\in \mathrm{V}$
5 fveq2 ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}={\mathrm{Base}}_{{C}}$
6 5 1 syl6eqr ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}={B}$
7 fvexd ${⊢}\left({c}={C}\wedge {b}={B}\right)\to \mathrm{Hom}\left({c}\right)\in \mathrm{V}$
8 simpl ${⊢}\left({c}={C}\wedge {b}={B}\right)\to {c}={C}$
9 8 fveq2d ${⊢}\left({c}={C}\wedge {b}={B}\right)\to \mathrm{Hom}\left({c}\right)=\mathrm{Hom}\left({C}\right)$
10 9 2 syl6eqr ${⊢}\left({c}={C}\wedge {b}={B}\right)\to \mathrm{Hom}\left({c}\right)={H}$
11 fvexd ${⊢}\left(\left({c}={C}\wedge {b}={B}\right)\wedge {h}={H}\right)\to \mathrm{comp}\left({c}\right)\in \mathrm{V}$
12 simpll ${⊢}\left(\left({c}={C}\wedge {b}={B}\right)\wedge {h}={H}\right)\to {c}={C}$
13 12 fveq2d ${⊢}\left(\left({c}={C}\wedge {b}={B}\right)\wedge {h}={H}\right)\to \mathrm{comp}\left({c}\right)=\mathrm{comp}\left({C}\right)$
14 13 3 syl6eqr
15 simpllr
16 simplr
17 16 oveqd
18 16 oveqd
19 simpr
20 19 oveqd
21 20 oveqd
22 21 eqeq1d
23 18 22 raleqbidv
24 16 oveqd
25 19 oveqd
26 25 oveqd
27 26 eqeq1d
28 24 27 raleqbidv
29 23 28 anbi12d
30 15 29 raleqbidv
31 17 30 rexeqbidv
32 16 oveqd
33 19 oveqd
34 33 oveqd
35 16 oveqd
36 34 35 eleq12d
37 16 oveqd
38 19 oveqd
39 19 oveqd
40 39 oveqd
41 eqidd
42 38 40 41 oveq123d
43 19 oveqd
44 eqidd
45 43 44 34 oveq123d
46 42 45 eqeq12d
47 37 46 raleqbidv
48 15 47 raleqbidv
49 36 48 anbi12d
50 32 49 raleqbidv
51 24 50 raleqbidv
52 15 51 raleqbidv
53 15 52 raleqbidv
54 31 53 anbi12d
55 15 54 raleqbidv
56 11 14 55 sbcied2
57 7 10 56 sbcied2
58 4 6 57 sbcied2
59 df-cat
60 58 59 elab2g