# Metamath Proof Explorer

## Theorem subccocl

Description: A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcidcl.j ${⊢}{\phi }\to {J}\in \mathrm{Subcat}\left({C}\right)$
subcidcl.2 ${⊢}{\phi }\to {J}Fn\left({S}×{S}\right)$
subcidcl.x ${⊢}{\phi }\to {X}\in {S}$
subccocl.o
subccocl.y ${⊢}{\phi }\to {Y}\in {S}$
subccocl.z ${⊢}{\phi }\to {Z}\in {S}$
subccocl.f ${⊢}{\phi }\to {F}\in \left({X}{J}{Y}\right)$
subccocl.g ${⊢}{\phi }\to {G}\in \left({Y}{J}{Z}\right)$
Assertion subccocl

### Proof

Step Hyp Ref Expression
1 subcidcl.j ${⊢}{\phi }\to {J}\in \mathrm{Subcat}\left({C}\right)$
2 subcidcl.2 ${⊢}{\phi }\to {J}Fn\left({S}×{S}\right)$
3 subcidcl.x ${⊢}{\phi }\to {X}\in {S}$
4 subccocl.o
5 subccocl.y ${⊢}{\phi }\to {Y}\in {S}$
6 subccocl.z ${⊢}{\phi }\to {Z}\in {S}$
7 subccocl.f ${⊢}{\phi }\to {F}\in \left({X}{J}{Y}\right)$
8 subccocl.g ${⊢}{\phi }\to {G}\in \left({Y}{J}{Z}\right)$
9 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({C}\right)$
10 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
11 subcrcl ${⊢}{J}\in \mathrm{Subcat}\left({C}\right)\to {C}\in \mathrm{Cat}$
12 1 11 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
13 9 10 4 12 2 issubc2
14 1 13 mpbid
15 14 simprd
16 5 adantr ${⊢}\left({\phi }\wedge {x}={X}\right)\to {Y}\in {S}$
17 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {Z}\in {S}$
18 7 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {F}\in \left({X}{J}{Y}\right)$
19 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}={X}$
20 simplr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {y}={Y}$
21 19 20 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}{J}{y}={X}{J}{Y}$
22 18 21 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {F}\in \left({x}{J}{y}\right)$
23 8 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}{J}{Z}\right)$
24 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}$
25 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}$
26 24 25 oveq12d ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {f}={F}\right)\to {y}{J}{z}={Y}{J}{Z}$
27 23 26 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}{J}{z}\right)$
28 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}$
29 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}$
30 28 29 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}⟩$
31 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}$
32 30 31 oveq12d
33 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}$
34 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}$
35 32 33 34 oveq123d
36 28 31 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}{J}{z}={X}{J}{Z}$
37 35 36 eleq12d
38 27 37 rspcdv
39 22 38 rspcimdv
40 17 39 rspcimdv
41 16 40 rspcimdv