Metamath Proof Explorer

Theorem catcocl

Description: Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catcocl.b 
|- B = ( Base ` C )
catcocl.h 
|- H = ( Hom ` C )
catcocl.o 
|- .x. = ( comp ` C )
catcocl.c 
|- ( ph -> C e. Cat )
catcocl.x 
|- ( ph -> X e. B )
catcocl.y 
|- ( ph -> Y e. B )
catcocl.z 
|- ( ph -> Z e. B )
catcocl.f 
|- ( ph -> F e. ( X H Y ) )
catcocl.g 
|- ( ph -> G e. ( Y H Z ) )
Assertion catcocl 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) )

Proof

Step Hyp Ref Expression
1 catcocl.b 
 |-  B = ( Base ` C )
2 catcocl.h 
 |-  H = ( Hom ` C )
3 catcocl.o 
 |-  .x. = ( comp ` C )
4 catcocl.c 
 |-  ( ph -> C e. Cat )
5 catcocl.x 
 |-  ( ph -> X e. B )
6 catcocl.y 
 |-  ( ph -> Y e. B )
7 catcocl.z 
 |-  ( ph -> Z e. B )
8 catcocl.f 
 |-  ( ph -> F e. ( X H Y ) )
9 catcocl.g 
 |-  ( ph -> G e. ( Y H Z ) )
10 1 2 3 iscat 
 |-  ( C e. Cat -> ( C e. Cat <-> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
11 10 ibi 
 |-  ( C e. Cat -> A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
12 simpl 
 |-  ( ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
13 12 2ralimi 
 |-  ( A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
14 13 2ralimi 
 |-  ( A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
15 14 adantl 
 |-  ( ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
16 15 ralimi 
 |-  ( A. x e. B ( E. g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. v e. ( z H w ) ( ( v ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( v ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
17 4 11 16 3syl 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
18 6 adantr 
 |-  ( ( ph /\ x = X ) -> Y e. B )
19 7 ad2antrr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> Z e. B )
20 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( X H Y ) )
21 simpllr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> x = X )
22 simplr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> y = Y )
23 21 22 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( x H y ) = ( X H Y ) )
24 20 23 eleqtrrd 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( x H y ) )
25 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> G e. ( Y H Z ) )
26 simpr 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> z = Z )
27 22 26 oveq12d 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( y H z ) = ( Y H Z ) )
28 25 27 eleqtrrd 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> G e. ( y H z ) )
29 28 adantr 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( y H z ) )
30 simp-5r 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> x = X )
31 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> y = Y )
32 30 31 opeq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> <. x , y >. = <. X , Y >. )
33 simpllr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> z = Z )
34 32 33 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( <. x , y >. .x. z ) = ( <. X , Y >. .x. Z ) )
35 simpr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> g = G )
36 simplr 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> f = F )
37 34 35 36 oveq123d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( g ( <. x , y >. .x. z ) f ) = ( G ( <. X , Y >. .x. Z ) F ) )
38 30 33 oveq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( x H z ) = ( X H Z ) )
39 37 38 eleq12d 
 |-  ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
40 29 39 rspcdv 
 |-  ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
41 24 40 rspcimdv 
 |-  ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
42 19 41 rspcimdv 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
43 18 42 rspcimdv 
 |-  ( ( ph /\ x = X ) -> ( A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
44 5 43 rspcimdv 
 |-  ( ph -> ( A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
45 17 44 mpd 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) )