Metamath Proof Explorer


Theorem subccocl

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

Ref Expression
Hypotheses subcidcl.j
|- ( ph -> J e. ( Subcat ` C ) )
subcidcl.2
|- ( ph -> J Fn ( S X. S ) )
subcidcl.x
|- ( ph -> X e. S )
subccocl.o
|- .x. = ( comp ` C )
subccocl.y
|- ( ph -> Y e. S )
subccocl.z
|- ( ph -> Z e. S )
subccocl.f
|- ( ph -> F e. ( X J Y ) )
subccocl.g
|- ( ph -> G e. ( Y J Z ) )
Assertion subccocl
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) )

Proof

Step Hyp Ref Expression
1 subcidcl.j
 |-  ( ph -> J e. ( Subcat ` C ) )
2 subcidcl.2
 |-  ( ph -> J Fn ( S X. S ) )
3 subcidcl.x
 |-  ( ph -> X e. S )
4 subccocl.o
 |-  .x. = ( comp ` C )
5 subccocl.y
 |-  ( ph -> Y e. S )
6 subccocl.z
 |-  ( ph -> Z e. S )
7 subccocl.f
 |-  ( ph -> F e. ( X J Y ) )
8 subccocl.g
 |-  ( ph -> G e. ( Y J Z ) )
9 eqid
 |-  ( Homf ` C ) = ( Homf ` C )
10 eqid
 |-  ( Id ` C ) = ( Id ` C )
11 subcrcl
 |-  ( J e. ( Subcat ` C ) -> C e. Cat )
12 1 11 syl
 |-  ( ph -> C e. Cat )
13 9 10 4 12 2 issubc2
 |-  ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) ) ) )
14 1 13 mpbid
 |-  ( ph -> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) ) )
15 14 simprd
 |-  ( ph -> A. x e. S ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) )
16 5 adantr
 |-  ( ( ph /\ x = X ) -> Y e. S )
17 6 ad2antrr
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> Z e. S )
18 7 ad3antrrr
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( X J Y ) )
19 simpllr
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> x = X )
20 simplr
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> y = Y )
21 19 20 oveq12d
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( x J y ) = ( X J Y ) )
22 18 21 eleqtrrd
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( x J y ) )
23 8 ad4antr
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( Y J Z ) )
24 simpllr
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> y = Y )
25 simplr
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> z = Z )
26 24 25 oveq12d
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( y J z ) = ( Y J Z ) )
27 23 26 eleqtrrd
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( y J z ) )
28 simp-5r
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> x = X )
29 simp-4r
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> y = Y )
30 28 29 opeq12d
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> <. x , y >. = <. X , Y >. )
31 simpllr
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> z = Z )
32 30 31 oveq12d
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( <. x , y >. .x. z ) = ( <. X , Y >. .x. Z ) )
33 simpr
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> g = G )
34 simplr
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> f = F )
35 32 33 34 oveq123d
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( g ( <. x , y >. .x. z ) f ) = ( G ( <. X , Y >. .x. Z ) F ) )
36 28 31 oveq12d
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( x J z ) = ( X J Z ) )
37 35 36 eleq12d
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) <-> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
38 27 37 rspcdv
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
39 22 38 rspcimdv
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
40 17 39 rspcimdv
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
41 16 40 rspcimdv
 |-  ( ( ph /\ x = X ) -> ( A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
42 41 adantld
 |-  ( ( ph /\ x = X ) -> ( ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
43 3 42 rspcimdv
 |-  ( ph -> ( A. x e. S ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) )
44 15 43 mpd
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) )