# Metamath Proof Explorer

## Theorem catcocl

Description: Closure of a composition arrow. (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)$
Assertion catcocl

### 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 1 2 3 iscat
11 10 ibi
12 simpl
13 12 2ralimi
14 13 2ralimi
16 15 ralimi
17 4 11 16 3syl
18 6 adantr ${⊢}\left({\phi }\wedge {x}={X}\right)\to {Y}\in {B}$
19 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {Z}\in {B}$
20 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)$
21 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}={X}$
22 simplr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {y}={Y}$
23 21 22 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}{H}{y}={X}{H}{Y}$
24 20 23 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)$
25 9 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {G}\in \left({Y}{H}{Z}\right)$
26 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {z}={Z}$
27 22 26 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {y}{H}{z}={Y}{H}{Z}$
28 25 27 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {G}\in \left({y}{H}{z}\right)$
29 28 adantr ${⊢}\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)$
30 simp-5r ${⊢}\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 {x}={X}$
31 simp-4r ${⊢}\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 {y}={Y}$
32 30 31 opeq12d ${⊢}\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 ⟨{x},{y}⟩=⟨{X},{Y}⟩$
33 simpllr ${⊢}\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 {z}={Z}$
34 32 33 oveq12d
35 simpr ${⊢}\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 {g}={G}$
36 simplr ${⊢}\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 {f}={F}$
37 34 35 36 oveq123d
38 30 33 oveq12d ${⊢}\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 {x}{H}{z}={X}{H}{Z}$
39 37 38 eleq12d
40 29 39 rspcdv
41 24 40 rspcimdv
42 19 41 rspcimdv
43 18 42 rspcimdv
44 5 43 rspcimdv
45 17 44 mpd