# Metamath Proof Explorer

## Theorem catass

Description: Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catcocl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
catcocl.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
catcocl.o
catcocl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
catcocl.x ${⊢}{\phi }\to {X}\in {B}$
catcocl.y ${⊢}{\phi }\to {Y}\in {B}$
catcocl.z ${⊢}{\phi }\to {Z}\in {B}$
catcocl.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
catcocl.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
catass.w ${⊢}{\phi }\to {W}\in {B}$
catass.g ${⊢}{\phi }\to {K}\in \left({Z}{H}{W}\right)$
Assertion catass

### Proof

Step Hyp Ref Expression
1 catcocl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 catcocl.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 catcocl.o
4 catcocl.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 catcocl.x ${⊢}{\phi }\to {X}\in {B}$
6 catcocl.y ${⊢}{\phi }\to {Y}\in {B}$
7 catcocl.z ${⊢}{\phi }\to {Z}\in {B}$
8 catcocl.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
9 catcocl.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
10 catass.w ${⊢}{\phi }\to {W}\in {B}$
11 catass.g ${⊢}{\phi }\to {K}\in \left({Z}{H}{W}\right)$
12 1 2 3 iscat
13 12 ibi
14 4 13 syl
15 6 adantr ${⊢}\left({\phi }\wedge {x}={X}\right)\to {Y}\in {B}$
16 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {Z}\in {B}$
17 8 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {F}\in \left({X}{H}{Y}\right)$
18 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}={X}$
19 simplr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {y}={Y}$
20 18 19 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}{H}{y}={X}{H}{Y}$
21 17 20 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {F}\in \left({x}{H}{y}\right)$
22 9 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\to {G}\in \left({Y}{H}{Z}\right)$
23 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\to {y}={Y}$
24 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\to {z}={Z}$
25 23 24 oveq12d ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\to {y}{H}{z}={Y}{H}{Z}$
26 22 25 eleqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\to {G}\in \left({y}{H}{z}\right)$
27 10 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\to {W}\in {B}$
28 11 ad6antr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\to {K}\in \left({Z}{H}{W}\right)$
29 simp-4r ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\to {z}={Z}$
30 simpr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\to {w}={W}$
31 29 30 oveq12d ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\to {z}{H}{w}={Z}{H}{W}$
32 28 31 eleqtrrd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\to {K}\in \left({z}{H}{w}\right)$
33 simp-7r ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {x}={X}$
34 simp-6r ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {y}={Y}$
35 33 34 opeq12d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to ⟨{x},{y}⟩=⟨{X},{Y}⟩$
36 simplr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {w}={W}$
37 35 36 oveq12d
38 simp-5r ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {z}={Z}$
39 34 38 opeq12d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to ⟨{y},{z}⟩=⟨{Y},{Z}⟩$
40 39 36 oveq12d
41 simpr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {k}={K}$
42 simpllr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {g}={G}$
43 40 41 42 oveq123d
44 simp-4r ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to {f}={F}$
45 37 43 44 oveq123d
46 33 38 opeq12d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\wedge {g}={G}\right)\wedge {w}={W}\right)\wedge {k}={K}\right)\to ⟨{x},{z}⟩=⟨{X},{Z}⟩$
47 46 36 oveq12d
48 35 38 oveq12d
49 48 42 44 oveq123d
50 47 41 49 oveq123d
51 45 50 eqeq12d
52 32 51 rspcdv
53 27 52 rspcimdv