Metamath Proof Explorer


Theorem subccocl

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

Ref Expression
Hypotheses subcidcl.j φJSubcatC
subcidcl.2 φJFnS×S
subcidcl.x φXS
subccocl.o ·˙=compC
subccocl.y φYS
subccocl.z φZS
subccocl.f φFXJY
subccocl.g φGYJZ
Assertion subccocl φGXY·˙ZFXJZ

Proof

Step Hyp Ref Expression
1 subcidcl.j φJSubcatC
2 subcidcl.2 φJFnS×S
3 subcidcl.x φXS
4 subccocl.o ·˙=compC
5 subccocl.y φYS
6 subccocl.z φZS
7 subccocl.f φFXJY
8 subccocl.g φGYJZ
9 eqid Hom𝑓C=Hom𝑓C
10 eqid IdC=IdC
11 subcrcl JSubcatCCCat
12 1 11 syl φCCat
13 9 10 4 12 2 issubc2 φJSubcatCJcatHom𝑓CxSIdCxxJxySzSfxJygyJzgxy·˙zfxJz
14 1 13 mpbid φJcatHom𝑓CxSIdCxxJxySzSfxJygyJzgxy·˙zfxJz
15 14 simprd φxSIdCxxJxySzSfxJygyJzgxy·˙zfxJz
16 5 adantr φx=XYS
17 6 ad2antrr φx=Xy=YZS
18 7 ad3antrrr φx=Xy=Yz=ZFXJY
19 simpllr φx=Xy=Yz=Zx=X
20 simplr φx=Xy=Yz=Zy=Y
21 19 20 oveq12d φx=Xy=Yz=ZxJy=XJY
22 18 21 eleqtrrd φx=Xy=Yz=ZFxJy
23 8 ad4antr φx=Xy=Yz=Zf=FGYJZ
24 simpllr φx=Xy=Yz=Zf=Fy=Y
25 simplr φx=Xy=Yz=Zf=Fz=Z
26 24 25 oveq12d φx=Xy=Yz=Zf=FyJz=YJZ
27 23 26 eleqtrrd φx=Xy=Yz=Zf=FGyJz
28 simp-5r φx=Xy=Yz=Zf=Fg=Gx=X
29 simp-4r φx=Xy=Yz=Zf=Fg=Gy=Y
30 28 29 opeq12d φx=Xy=Yz=Zf=Fg=Gxy=XY
31 simpllr φx=Xy=Yz=Zf=Fg=Gz=Z
32 30 31 oveq12d φx=Xy=Yz=Zf=Fg=Gxy·˙z=XY·˙Z
33 simpr φx=Xy=Yz=Zf=Fg=Gg=G
34 simplr φx=Xy=Yz=Zf=Fg=Gf=F
35 32 33 34 oveq123d φx=Xy=Yz=Zf=Fg=Ggxy·˙zf=GXY·˙ZF
36 28 31 oveq12d φx=Xy=Yz=Zf=Fg=GxJz=XJZ
37 35 36 eleq12d φx=Xy=Yz=Zf=Fg=Ggxy·˙zfxJzGXY·˙ZFXJZ
38 27 37 rspcdv φx=Xy=Yz=Zf=FgyJzgxy·˙zfxJzGXY·˙ZFXJZ
39 22 38 rspcimdv φx=Xy=Yz=ZfxJygyJzgxy·˙zfxJzGXY·˙ZFXJZ
40 17 39 rspcimdv φx=Xy=YzSfxJygyJzgxy·˙zfxJzGXY·˙ZFXJZ
41 16 40 rspcimdv φx=XySzSfxJygyJzgxy·˙zfxJzGXY·˙ZFXJZ
42 41 adantld φx=XIdCxxJxySzSfxJygyJzgxy·˙zfxJzGXY·˙ZFXJZ
43 3 42 rspcimdv φxSIdCxxJxySzSfxJygyJzgxy·˙zfxJzGXY·˙ZFXJZ
44 15 43 mpd φGXY·˙ZFXJZ