Metamath Proof Explorer

Theorem xpccatid

Description: The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses xpccat.t 
|- T = ( C Xc. D )
xpccat.c 
|- ( ph -> C e. Cat )
xpccat.d 
|- ( ph -> D e. Cat )
xpccat.x 
|- X = ( Base ` C )
xpccat.y 
|- Y = ( Base ` D )
xpccat.i 
|- I = ( Id ` C )
xpccat.j 
|- J = ( Id ` D )
Assertion xpccatid 
|- ( ph -> ( T e. Cat /\ ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) ) )

Proof

Step Hyp Ref Expression
1 xpccat.t 
 |-  T = ( C Xc. D )
2 xpccat.c 
 |-  ( ph -> C e. Cat )
3 xpccat.d 
 |-  ( ph -> D e. Cat )
4 xpccat.x 
 |-  X = ( Base ` C )
5 xpccat.y 
 |-  Y = ( Base ` D )
6 xpccat.i 
 |-  I = ( Id ` C )
7 xpccat.j 
 |-  J = ( Id ` D )
8 1 4 5 xpcbas 
 |-  ( X X. Y ) = ( Base ` T )
9 8 a1i 
 |-  ( ph -> ( X X. Y ) = ( Base ` T ) )
10 eqidd 
 |-  ( ph -> ( Hom ` T ) = ( Hom ` T ) )
11 eqidd 
 |-  ( ph -> ( comp ` T ) = ( comp ` T ) )
12 1 ovexi 
 |-  T e. _V
13 12 a1i 
 |-  ( ph -> T e. _V )
14 biid 
 |-  ( ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) <-> ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) )
15 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
16 2 adantr 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> C e. Cat )
17 xp1st 
 |-  ( t e. ( X X. Y ) -> ( 1st ` t ) e. X )
18 17 adantl 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> ( 1st ` t ) e. X )
19 4 15 6 16 18 catidcl 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> ( I ` ( 1st ` t ) ) e. ( ( 1st ` t ) ( Hom ` C ) ( 1st ` t ) ) )
20 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
21 3 adantr 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> D e. Cat )
22 xp2nd 
 |-  ( t e. ( X X. Y ) -> ( 2nd ` t ) e. Y )
23 22 adantl 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> ( 2nd ` t ) e. Y )
24 5 20 7 21 23 catidcl 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> ( J ` ( 2nd ` t ) ) e. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` t ) ) )
25 19 24 opelxpd 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. e. ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` t ) ) ) )
26 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
27 simpr 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> t e. ( X X. Y ) )
28 1 8 15 20 26 27 27 xpchom 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> ( t ( Hom ` T ) t ) = ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` t ) ) ) )
29 25 28 eleqtrrd 
 |-  ( ( ph /\ t e. ( X X. Y ) ) -> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. e. ( t ( Hom ` T ) t ) )
30 fvex 
 |-  ( I ` ( 1st ` t ) ) e. _V
31 fvex 
 |-  ( J ` ( 2nd ` t ) ) e. _V
32 30 31 op1st 
 |-  ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) = ( I ` ( 1st ` t ) )
33 32 oveq1i 
 |-  ( ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` t ) ) ( 1st ` f ) ) = ( ( I ` ( 1st ` t ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` t ) ) ( 1st ` f ) )
34 2 adantr 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> C e. Cat )
35 simpr1l 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> s e. ( X X. Y ) )
36 xp1st 
 |-  ( s e. ( X X. Y ) -> ( 1st ` s ) e. X )
37 35 36 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` s ) e. X )
38 eqid 
 |-  ( comp ` C ) = ( comp ` C )
39 simpr1r 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> t e. ( X X. Y ) )
40 39 17 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` t ) e. X )
41 simpr31 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> f e. ( s ( Hom ` T ) t ) )
42 1 8 15 20 26 35 39 xpchom 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( s ( Hom ` T ) t ) = ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) ) )
43 41 42 eleqtrd 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> f e. ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) ) )
44 xp1st 
 |-  ( f e. ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) ) -> ( 1st ` f ) e. ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) )
45 43 44 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` f ) e. ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) )
46 4 15 6 34 37 38 40 45 catlid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( I ` ( 1st ` t ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` t ) ) ( 1st ` f ) ) = ( 1st ` f ) )
47 33 46 eqtrid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` t ) ) ( 1st ` f ) ) = ( 1st ` f ) )
48 30 31 op2nd 
 |-  ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) = ( J ` ( 2nd ` t ) )
49 48 oveq1i 
 |-  ( ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` t ) ) ( 2nd ` f ) ) = ( ( J ` ( 2nd ` t ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` t ) ) ( 2nd ` f ) )
50 3 adantr 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> D e. Cat )
51 xp2nd 
 |-  ( s e. ( X X. Y ) -> ( 2nd ` s ) e. Y )
52 35 51 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` s ) e. Y )
53 eqid 
 |-  ( comp ` D ) = ( comp ` D )
54 39 22 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` t ) e. Y )
55 xp2nd 
 |-  ( f e. ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) ) -> ( 2nd ` f ) e. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) )
56 43 55 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` f ) e. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) )
57 5 20 7 50 52 53 54 56 catlid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( J ` ( 2nd ` t ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` t ) ) ( 2nd ` f ) ) = ( 2nd ` f ) )
58 49 57 eqtrid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` t ) ) ( 2nd ` f ) ) = ( 2nd ` f ) )
59 47 58 opeq12d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> <. ( ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` t ) ) ( 1st ` f ) ) , ( ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` t ) ) ( 2nd ` f ) ) >. = <. ( 1st ` f ) , ( 2nd ` f ) >. )
60 eqid 
 |-  ( comp ` T ) = ( comp ` T )
61 39 29 syldan 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. e. ( t ( Hom ` T ) t ) )
62 1 8 26 38 53 60 35 39 39 41 61 xpcco 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ( <. s , t >. ( comp ` T ) t ) f ) = <. ( ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` t ) ) ( 1st ` f ) ) , ( ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` t ) ) ( 2nd ` f ) ) >. )
63 1st2nd2 
 |-  ( f e. ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` t ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` t ) ) ) -> f = <. ( 1st ` f ) , ( 2nd ` f ) >. )
64 43 63 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> f = <. ( 1st ` f ) , ( 2nd ` f ) >. )
65 59 62 64 3eqtr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ( <. s , t >. ( comp ` T ) t ) f ) = f )
66 32 oveq2i 
 |-  ( ( 1st ` g ) ( <. ( 1st ` t ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) = ( ( 1st ` g ) ( <. ( 1st ` t ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( I ` ( 1st ` t ) ) )
67 simpr2l 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> u e. ( X X. Y ) )
68 xp1st 
 |-  ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )
69 67 68 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` u ) e. X )
70 simpr32 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> g e. ( t ( Hom ` T ) u ) )
71 1 8 15 20 26 39 67 xpchom 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( t ( Hom ` T ) u ) = ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) ) )
72 70 71 eleqtrd 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> g e. ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) ) )
73 xp1st 
 |-  ( g e. ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) ) -> ( 1st ` g ) e. ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) )
74 72 73 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` g ) e. ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) )
75 4 15 6 34 40 38 69 74 catrid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` g ) ( <. ( 1st ` t ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( I ` ( 1st ` t ) ) ) = ( 1st ` g ) )
76 66 75 eqtrid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` g ) ( <. ( 1st ` t ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) = ( 1st ` g ) )
77 48 oveq2i 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` t ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` t ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( J ` ( 2nd ` t ) ) )
78 xp2nd 
 |-  ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )
79 67 78 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` u ) e. Y )
80 xp2nd 
 |-  ( g e. ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) )
81 72 80 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) )
82 5 20 7 50 54 53 79 81 catrid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` g ) ( <. ( 2nd ` t ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( J ` ( 2nd ` t ) ) ) = ( 2nd ` g ) )
83 77 82 eqtrid 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` g ) ( <. ( 2nd ` t ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) = ( 2nd ` g ) )
84 76 83 opeq12d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` t ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` t ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) >. = <. ( 1st ` g ) , ( 2nd ` g ) >. )
85 1 8 26 38 53 60 39 39 67 61 70 xpcco 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( g ( <. t , t >. ( comp ` T ) u ) <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) = <. ( ( 1st ` g ) ( <. ( 1st ` t ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` t ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) >. )
86 1st2nd2 
 |-  ( g e. ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` u ) ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
87 72 86 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
88 84 85 87 3eqtr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( g ( <. t , t >. ( comp ` T ) u ) <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) = g )
89 4 15 38 34 37 40 69 45 74 catcocl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) e. ( ( 1st ` s ) ( Hom ` C ) ( 1st ` u ) ) )
90 5 20 53 50 52 54 79 56 81 catcocl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) e. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` u ) ) )
91 89 90 opelxpd 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) >. e. ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` u ) ) ) )
92 1 8 26 38 53 60 35 39 67 41 70 xpcco 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( g ( <. s , t >. ( comp ` T ) u ) f ) = <. ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) >. )
93 1 8 15 20 26 35 67 xpchom 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( s ( Hom ` T ) u ) = ( ( ( 1st ` s ) ( Hom ` C ) ( 1st ` u ) ) X. ( ( 2nd ` s ) ( Hom ` D ) ( 2nd ` u ) ) ) )
94 91 92 93 3eltr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( g ( <. s , t >. ( comp ` T ) u ) f ) e. ( s ( Hom ` T ) u ) )
95 simpr2r 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> v e. ( X X. Y ) )
96 xp1st 
 |-  ( v e. ( X X. Y ) -> ( 1st ` v ) e. X )
97 95 96 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` v ) e. X )
98 simpr33 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> h e. ( u ( Hom ` T ) v ) )
99 1 8 15 20 26 67 95 xpchom 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( u ( Hom ` T ) v ) = ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) )
100 98 99 eleqtrd 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> h e. ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) )
101 xp1st 
 |-  ( h e. ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) -> ( 1st ` h ) e. ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) )
102 100 101 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` h ) e. ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) )
103 4 15 38 34 37 40 69 45 74 97 102 catass 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` f ) ) = ( ( 1st ` h ) ( <. ( 1st ` s ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) ) )
104 1 8 26 38 53 60 39 67 95 70 98 xpcco 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( h ( <. t , u >. ( comp ` T ) v ) g ) = <. ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) >. )
105 104 fveq2d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) = ( 1st ` <. ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) >. ) )
106 ovex 
 |-  ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) e. _V
107 ovex 
 |-  ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) e. _V
108 106 107 op1st 
 |-  ( 1st ` <. ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) >. ) = ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) )
109 105 108 eqtrdi 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) = ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) )
110 109 oveq1d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` f ) ) = ( ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` f ) ) )
111 92 fveq2d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) = ( 1st ` <. ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) >. ) )
112 ovex 
 |-  ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) e. _V
113 ovex 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) e. _V
114 112 113 op1st 
 |-  ( 1st ` <. ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) >. ) = ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) )
115 111 114 eqtrdi 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 1st ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) = ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) )
116 115 oveq2d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` h ) ( <. ( 1st ` s ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) = ( ( 1st ` h ) ( <. ( 1st ` s ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) ) )
117 103 110 116 3eqtr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` f ) ) = ( ( 1st ` h ) ( <. ( 1st ` s ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) )
118 xp2nd 
 |-  ( v e. ( X X. Y ) -> ( 2nd ` v ) e. Y )
119 95 118 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` v ) e. Y )
120 xp2nd 
 |-  ( h e. ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) -> ( 2nd ` h ) e. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) )
121 100 120 syl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` h ) e. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) )
122 5 20 53 50 52 54 79 56 81 119 121 catass 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` f ) ) = ( ( 2nd ` h ) ( <. ( 2nd ` s ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) ) )
123 104 fveq2d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) = ( 2nd ` <. ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) >. ) )
124 106 107 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) >. ) = ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) )
125 123 124 eqtrdi 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) = ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) )
126 125 oveq1d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` f ) ) = ( ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` f ) ) )
127 92 fveq2d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) = ( 2nd ` <. ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) >. ) )
128 112 113 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` g ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` u ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) >. ) = ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) )
129 127 128 eqtrdi 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( 2nd ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) )
130 129 oveq2d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` h ) ( <. ( 2nd ` s ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) = ( ( 2nd ` h ) ( <. ( 2nd ` s ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( ( 2nd ` g ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` u ) ) ( 2nd ` f ) ) ) )
131 122 126 130 3eqtr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` f ) ) = ( ( 2nd ` h ) ( <. ( 2nd ` s ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) )
132 117 131 opeq12d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> <. ( ( 1st ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` f ) ) , ( ( 2nd ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` f ) ) >. = <. ( ( 1st ` h ) ( <. ( 1st ` s ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` s ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) >. )
133 4 15 38 34 40 69 97 74 102 catcocl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) e. ( ( 1st ` t ) ( Hom ` C ) ( 1st ` v ) ) )
134 5 20 53 50 54 79 119 81 121 catcocl 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) e. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` v ) ) )
135 133 134 opelxpd 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> <. ( ( 1st ` h ) ( <. ( 1st ` t ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` g ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` t ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` g ) ) >. e. ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` v ) ) ) )
136 1 8 15 20 26 39 95 xpchom 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( t ( Hom ` T ) v ) = ( ( ( 1st ` t ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` t ) ( Hom ` D ) ( 2nd ` v ) ) ) )
137 135 104 136 3eltr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( h ( <. t , u >. ( comp ` T ) v ) g ) e. ( t ( Hom ` T ) v ) )
138 1 8 26 38 53 60 35 39 95 41 137 xpcco 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( h ( <. t , u >. ( comp ` T ) v ) g ) ( <. s , t >. ( comp ` T ) v ) f ) = <. ( ( 1st ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 1st ` s ) , ( 1st ` t ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` f ) ) , ( ( 2nd ` ( h ( <. t , u >. ( comp ` T ) v ) g ) ) ( <. ( 2nd ` s ) , ( 2nd ` t ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` f ) ) >. )
139 1 8 26 38 53 60 35 67 95 94 98 xpcco 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( h ( <. s , u >. ( comp ` T ) v ) ( g ( <. s , t >. ( comp ` T ) u ) f ) ) = <. ( ( 1st ` h ) ( <. ( 1st ` s ) , ( 1st ` u ) >. ( comp ` C ) ( 1st ` v ) ) ( 1st ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) , ( ( 2nd ` h ) ( <. ( 2nd ` s ) , ( 2nd ` u ) >. ( comp ` D ) ( 2nd ` v ) ) ( 2nd ` ( g ( <. s , t >. ( comp ` T ) u ) f ) ) ) >. )
140 132 138 139 3eqtr4d 
 |-  ( ( ph /\ ( ( s e. ( X X. Y ) /\ t e. ( X X. Y ) ) /\ ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) /\ ( f e. ( s ( Hom ` T ) t ) /\ g e. ( t ( Hom ` T ) u ) /\ h e. ( u ( Hom ` T ) v ) ) ) ) -> ( ( h ( <. t , u >. ( comp ` T ) v ) g ) ( <. s , t >. ( comp ` T ) v ) f ) = ( h ( <. s , u >. ( comp ` T ) v ) ( g ( <. s , t >. ( comp ` T ) u ) f ) ) )
141 9 10 11 13 14 29 65 88 94 140 iscatd2 
 |-  ( ph -> ( T e. Cat /\ ( Id ` T ) = ( t e. ( X X. Y ) |-> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) )
142 vex 
 |-  x e. _V
143 vex 
 |-  y e. _V
144 142 143 op1std 
 |-  ( t = <. x , y >. -> ( 1st ` t ) = x )
145 144 fveq2d 
 |-  ( t = <. x , y >. -> ( I ` ( 1st ` t ) ) = ( I ` x ) )
146 142 143 op2ndd 
 |-  ( t = <. x , y >. -> ( 2nd ` t ) = y )
147 146 fveq2d 
 |-  ( t = <. x , y >. -> ( J ` ( 2nd ` t ) ) = ( J ` y ) )
148 145 147 opeq12d 
 |-  ( t = <. x , y >. -> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. = <. ( I ` x ) , ( J ` y ) >. )
149 148 mpompt 
 |-  ( t e. ( X X. Y ) |-> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. )
150 149 eqeq2i 
 |-  ( ( Id ` T ) = ( t e. ( X X. Y ) |-> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) <-> ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) )
151 150 anbi2i 
 |-  ( ( T e. Cat /\ ( Id ` T ) = ( t e. ( X X. Y ) |-> <. ( I ` ( 1st ` t ) ) , ( J ` ( 2nd ` t ) ) >. ) ) <-> ( T e. Cat /\ ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) ) )
152 141 151 sylib 
 |-  ( ph -> ( T e. Cat /\ ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) ) )