# Metamath Proof Explorer

## Theorem iscatd

Description: Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses iscatd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
iscatd.h ${⊢}{\phi }\to {H}=\mathrm{Hom}\left({C}\right)$
iscatd.o
iscatd.c ${⊢}{\phi }\to {C}\in {V}$
iscatd.1
iscatd.2
iscatd.3
iscatd.4
iscatd.5
Assertion iscatd ${⊢}{\phi }\to {C}\in \mathrm{Cat}$

### Proof

Step Hyp Ref Expression
1 iscatd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
2 iscatd.h ${⊢}{\phi }\to {H}=\mathrm{Hom}\left({C}\right)$
3 iscatd.o
4 iscatd.c ${⊢}{\phi }\to {C}\in {V}$
5 iscatd.1
6 iscatd.2
7 iscatd.3
8 iscatd.4
9 iscatd.5
10 6 3exp2
11 10 imp31
12 11 ralrimiv
13 7 3exp2
14 13 imp31
15 14 ralrimiv
16 12 15 jca
17 16 ralrimiva
18 oveq1
19 18 eqeq1d
20 19 ralbidv
21 oveq2
22 21 eqeq1d
23 22 ralbidv
24 20 23 anbi12d
25 24 ralbidv
26 25 rspcev
27 5 17 26 syl2anc
28 8 3expia
29 28 3exp2
30 29 imp43
31 9 3expa
32 31 3exp2
33 32 imp32
34 33 ralrimiv
35 34 ex
36 35 expr
37 36 expd
38 37 expr
39 38 imp42
40 39 ralrimdva
42 41 ralrimivv
43 42 ralrimivva
44 27 43 jca
45 44 ralrimiva
46 2 oveqd ${⊢}{\phi }\to {x}{H}{x}={x}\mathrm{Hom}\left({C}\right){x}$
47 2 oveqd ${⊢}{\phi }\to {y}{H}{x}={y}\mathrm{Hom}\left({C}\right){x}$
48 3 oveqd
49 48 oveqd
50 49 eqeq1d
51 47 50 raleqbidv
52 2 oveqd ${⊢}{\phi }\to {x}{H}{y}={x}\mathrm{Hom}\left({C}\right){y}$
53 3 oveqd
54 53 oveqd
55 54 eqeq1d
56 52 55 raleqbidv
57 51 56 anbi12d
58 1 57 raleqbidv
59 46 58 rexeqbidv
60 2 oveqd ${⊢}{\phi }\to {y}{H}{z}={y}\mathrm{Hom}\left({C}\right){z}$
61 3 oveqd
62 61 oveqd
63 2 oveqd ${⊢}{\phi }\to {x}{H}{z}={x}\mathrm{Hom}\left({C}\right){z}$
64 62 63 eleq12d
65 2 oveqd ${⊢}{\phi }\to {z}{H}{w}={z}\mathrm{Hom}\left({C}\right){w}$
66 3 oveqd
67 3 oveqd
68 67 oveqd
69 eqidd ${⊢}{\phi }\to {f}={f}$
70 66 68 69 oveq123d
71 3 oveqd
72 eqidd ${⊢}{\phi }\to {k}={k}$
73 71 72 62 oveq123d
74 70 73 eqeq12d
75 65 74 raleqbidv
76 1 75 raleqbidv
77 64 76 anbi12d
78 60 77 raleqbidv
79 52 78 raleqbidv
80 1 79 raleqbidv
81 1 80 raleqbidv
82 59 81 anbi12d
83 1 82 raleqbidv
84 45 83 mpbid ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge \forall {w}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}\mathrm{Hom}\left({C}\right){w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩\mathrm{comp}\left({C}\right){w}\right){g}\right)\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){w}\right){f}={k}\left(⟨{x},{z}⟩\mathrm{comp}\left({C}\right){w}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\right)\right)$
85 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
86 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
87 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
88 85 86 87 iscat ${⊢}{C}\in {V}\to \left({C}\in \mathrm{Cat}↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge \forall {w}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}\mathrm{Hom}\left({C}\right){w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩\mathrm{comp}\left({C}\right){w}\right){g}\right)\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){w}\right){f}={k}\left(⟨{x},{z}⟩\mathrm{comp}\left({C}\right){w}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\right)\right)\right)$
89 4 88 syl ${⊢}{\phi }\to \left({C}\in \mathrm{Cat}↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({x}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\left(\forall {f}\in \left({y}\mathrm{Hom}\left({C}\right){x}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{y},{x}⟩\mathrm{comp}\left({C}\right){x}\right){f}={f}\wedge \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{f}\left(⟨{x},{x}⟩\mathrm{comp}\left({C}\right){y}\right){g}={f}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\in \left({x}\mathrm{Hom}\left({C}\right){z}\right)\wedge \forall {w}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {k}\in \left({z}\mathrm{Hom}\left({C}\right){w}\right)\phantom{\rule{.4em}{0ex}}\left({k}\left(⟨{y},{z}⟩\mathrm{comp}\left({C}\right){w}\right){g}\right)\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){w}\right){f}={k}\left(⟨{x},{z}⟩\mathrm{comp}\left({C}\right){w}\right)\left({g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}\right)\right)\right)\right)$
90 84 89 mpbird ${⊢}{\phi }\to {C}\in \mathrm{Cat}$