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 ) )