Metamath Proof Explorer

Theorem prfcl

Description: The pairing of functors F : C --> D and G : C --> D is a functor <. F , G >. : C --> ( D X. E ) . (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prfcl.p 
|- P = ( F pairF G )
prfcl.t 
|- T = ( D Xc. E )
prfcl.c 
|- ( ph -> F e. ( C Func D ) )
prfcl.d 
|- ( ph -> G e. ( C Func E ) )
Assertion prfcl 
|- ( ph -> P e. ( C Func T ) )

Proof

Step Hyp Ref Expression
1 prfcl.p 
 |-  P = ( F pairF G )
2 prfcl.t 
 |-  T = ( D Xc. E )
3 prfcl.c 
 |-  ( ph -> F e. ( C Func D ) )
4 prfcl.d 
 |-  ( ph -> G e. ( C Func E ) )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 1 5 6 3 4 prfval 
 |-  ( ph -> P = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
8 fvex 
 |-  ( Base ` C ) e. _V
9 8 mptex 
 |-  ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) e. _V
10 8 8 mpoex 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) e. _V
11 9 10 op1std 
 |-  ( P = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. -> ( 1st ` P ) = ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
12 7 11 syl 
 |-  ( ph -> ( 1st ` P ) = ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
13 9 10 op2ndd 
 |-  ( P = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. -> ( 2nd ` P ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) )
14 7 13 syl 
 |-  ( ph -> ( 2nd ` P ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) )
15 12 14 opeq12d 
 |-  ( ph -> <. ( 1st ` P ) , ( 2nd ` P ) >. = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
16 7 15 eqtr4d 
 |-  ( ph -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 eqid 
 |-  ( Base ` E ) = ( Base ` E )
19 2 17 18 xpcbas 
 |-  ( ( Base ` D ) X. ( Base ` E ) ) = ( Base ` T )
20 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
21 eqid 
 |-  ( Id ` C ) = ( Id ` C )
22 eqid 
 |-  ( Id ` T ) = ( Id ` T )
23 eqid 
 |-  ( comp ` C ) = ( comp ` C )
24 eqid 
 |-  ( comp ` T ) = ( comp ` T )
25 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
26 3 25 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
27 26 simpld 
 |-  ( ph -> C e. Cat )
28 26 simprd 
 |-  ( ph -> D e. Cat )
29 funcrcl 
 |-  ( G e. ( C Func E ) -> ( C e. Cat /\ E e. Cat ) )
30 4 29 syl 
 |-  ( ph -> ( C e. Cat /\ E e. Cat ) )
31 30 simprd 
 |-  ( ph -> E e. Cat )
32 2 28 31 xpccat 
 |-  ( ph -> T e. Cat )
33 relfunc 
 |-  Rel ( C Func D )
34 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
35 33 3 34 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
36 5 17 35 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
37 36 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
38 relfunc 
 |-  Rel ( C Func E )
39 1st2ndbr 
 |-  ( ( Rel ( C Func E ) /\ G e. ( C Func E ) ) -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
40 38 4 39 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
41 5 18 40 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` E ) )
42 41 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` E ) )
43 37 42 opelxpd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. e. ( ( Base ` D ) X. ( Base ` E ) ) )
44 12 43 fmpt3d 
 |-  ( ph -> ( 1st ` P ) : ( Base ` C ) --> ( ( Base ` D ) X. ( Base ` E ) ) )
45 eqid 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) )
46 ovex 
 |-  ( x ( Hom ` C ) y ) e. _V
47 46 mptex 
 |-  ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) e. _V
48 45 47 fnmpoi 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) Fn ( ( Base ` C ) X. ( Base ` C ) )
49 14 fneq1d 
 |-  ( ph -> ( ( 2nd ` P ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
50 48 49 mpbiri 
 |-  ( ph -> ( 2nd ` P ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
51 14 oveqd 
 |-  ( ph -> ( x ( 2nd ` P ) y ) = ( x ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) y ) )
52 45 ovmpt4g 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) e. _V ) -> ( x ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) y ) = ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) )
53 47 52 mp3an3 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) y ) = ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) )
54 51 53 sylan9eq 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` P ) y ) = ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) )
55 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
56 35 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
57 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
58 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
59 5 6 55 56 57 58 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
60 59 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` F ) y ) ` h ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
61 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
62 40 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
63 5 6 61 62 57 58 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` G ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) )
64 63 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` G ) y ) ` h ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) )
65 60 64 opelxpd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. e. ( ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) X. ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) ) )
66 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F e. ( C Func D ) )
67 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> G e. ( C Func E ) )
68 1 5 6 66 67 57 prf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` P ) ` x ) = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. )
69 1 5 6 66 67 58 prf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` P ) ` y ) = <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. )
70 68 69 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` P ) ` x ) ( Hom ` T ) ( ( 1st ` P ) ` y ) ) = ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( Hom ` T ) <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. ) )
71 37 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
72 42 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` E ) )
73 36 ffvelrnda 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
74 73 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
75 41 ffvelrnda 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` E ) )
76 75 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` E ) )
77 2 17 18 55 61 71 72 74 76 20 xpchom2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( Hom ` T ) <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. ) = ( ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) X. ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) ) )
78 70 77 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` P ) ` x ) ( Hom ` T ) ( ( 1st ` P ) ` y ) ) = ( ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) X. ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) ) )
79 78 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( ( 1st ` P ) ` x ) ( Hom ` T ) ( ( 1st ` P ) ` y ) ) = ( ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) X. ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) ) )
80 65 79 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. e. ( ( ( 1st ` P ) ` x ) ( Hom ` T ) ( ( 1st ` P ) ` y ) ) )
81 54 80 fmpt3d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` P ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` P ) ` x ) ( Hom ` T ) ( ( 1st ` P ) ` y ) ) )
82 eqid 
 |-  ( Id ` D ) = ( Id ` D )
83 35 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
84 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
85 5 21 82 83 84 funcid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) )
86 eqid 
 |-  ( Id ` E ) = ( Id ` E )
87 40 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
88 5 21 86 87 84 funcid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` G ) ` x ) ) )
89 85 88 opeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) , ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) >. = <. ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) , ( ( Id ` E ) ` ( ( 1st ` G ) ` x ) ) >. )
90 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( C Func D ) )
91 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> G e. ( C Func E ) )
92 27 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
93 5 6 21 92 84 catidcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
94 1 5 6 90 91 84 84 93 prf2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` P ) x ) ` ( ( Id ` C ) ` x ) ) = <. ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) , ( ( x ( 2nd ` G ) x ) ` ( ( Id ` C ) ` x ) ) >. )
95 1 5 6 90 91 84 prf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` P ) ` x ) = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. )
96 95 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` T ) ` ( ( 1st ` P ) ` x ) ) = ( ( Id ` T ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
97 28 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
98 31 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E e. Cat )
99 2 97 98 17 18 82 86 22 37 42 xpcid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` T ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) = <. ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) , ( ( Id ` E ) ` ( ( 1st ` G ) ` x ) ) >. )
100 96 99 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` T ) ` ( ( 1st ` P ) ` x ) ) = <. ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) , ( ( Id ` E ) ` ( ( 1st ` G ) ` x ) ) >. )
101 89 94 100 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` P ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` T ) ` ( ( 1st ` P ) ` x ) ) )
102 eqid 
 |-  ( comp ` D ) = ( comp ` D )
103 35 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
104 simp21 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> x e. ( Base ` C ) )
105 simp22 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> y e. ( Base ` C ) )
106 simp23 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> z e. ( Base ` C ) )
107 simp3l 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> f e. ( x ( Hom ` C ) y ) )
108 simp3r 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> g e. ( y ( Hom ` C ) z ) )
109 5 6 23 102 103 104 105 106 107 108 funcco 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
110 eqid 
 |-  ( comp ` E ) = ( comp ` E )
111 4 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> G e. ( C Func E ) )
112 38 111 39 sylancr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
113 5 6 23 110 112 104 105 106 107 108 funcco 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` G ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` G ) z ) ` g ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` E ) ( ( 1st ` G ) ` z ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) )
114 109 113 opeq12d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> <. ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) , ( ( x ( 2nd ` G ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) >. = <. ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) , ( ( ( y ( 2nd ` G ) z ) ` g ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` E ) ( ( 1st ` G ) ` z ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) >. )
115 3 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> F e. ( C Func D ) )
116 27 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> C e. Cat )
117 5 6 23 116 104 105 106 107 108 catcocl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
118 1 5 6 115 111 104 106 117 prf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` P ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = <. ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) , ( ( x ( 2nd ` G ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) >. )
119 1 5 6 115 111 104 prf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` P ) ` x ) = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. )
120 1 5 6 115 111 105 prf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` P ) ` y ) = <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. )
121 119 120 opeq12d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> <. ( ( 1st ` P ) ` x ) , ( ( 1st ` P ) ` y ) >. = <. <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. , <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. >. )
122 1 5 6 115 111 106 prf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` P ) ` z ) = <. ( ( 1st ` F ) ` z ) , ( ( 1st ` G ) ` z ) >. )
123 121 122 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( <. ( ( 1st ` P ) ` x ) , ( ( 1st ` P ) ` y ) >. ( comp ` T ) ( ( 1st ` P ) ` z ) ) = ( <. <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. , <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. >. ( comp ` T ) <. ( ( 1st ` F ) ` z ) , ( ( 1st ` G ) ` z ) >. ) )
124 1 5 6 115 111 105 106 108 prf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( y ( 2nd ` P ) z ) ` g ) = <. ( ( y ( 2nd ` F ) z ) ` g ) , ( ( y ( 2nd ` G ) z ) ` g ) >. )
125 1 5 6 115 111 104 105 107 prf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` P ) y ) ` f ) = <. ( ( x ( 2nd ` F ) y ) ` f ) , ( ( x ( 2nd ` G ) y ) ` f ) >. )
126 123 124 125 oveq123d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( ( y ( 2nd ` P ) z ) ` g ) ( <. ( ( 1st ` P ) ` x ) , ( ( 1st ` P ) ` y ) >. ( comp ` T ) ( ( 1st ` P ) ` z ) ) ( ( x ( 2nd ` P ) y ) ` f ) ) = ( <. ( ( y ( 2nd ` F ) z ) ` g ) , ( ( y ( 2nd ` G ) z ) ` g ) >. ( <. <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. , <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. >. ( comp ` T ) <. ( ( 1st ` F ) ` z ) , ( ( 1st ` G ) ` z ) >. ) <. ( ( x ( 2nd ` F ) y ) ` f ) , ( ( x ( 2nd ` G ) y ) ` f ) >. ) )
127 36 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
128 127 104 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
129 41 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` E ) )
130 129 104 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` E ) )
131 127 105 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
132 129 105 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` E ) )
133 127 106 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` F ) ` z ) e. ( Base ` D ) )
134 129 106 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` G ) ` z ) e. ( Base ` E ) )
135 5 6 55 103 104 105 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
136 135 107 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
137 5 6 61 112 104 105 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( 2nd ` G ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) )
138 137 107 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` G ) y ) ` f ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` E ) ( ( 1st ` G ) ` y ) ) )
139 5 6 55 103 105 106 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( y ( 2nd ` F ) z ) : ( y ( Hom ` C ) z ) --> ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` z ) ) )
140 139 108 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( y ( 2nd ` F ) z ) ` g ) e. ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` z ) ) )
141 5 6 61 112 105 106 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( y ( 2nd ` G ) z ) : ( y ( Hom ` C ) z ) --> ( ( ( 1st ` G ) ` y ) ( Hom ` E ) ( ( 1st ` G ) ` z ) ) )
142 141 108 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( y ( 2nd ` G ) z ) ` g ) e. ( ( ( 1st ` G ) ` y ) ( Hom ` E ) ( ( 1st ` G ) ` z ) ) )
143 2 17 18 55 61 128 130 131 132 102 110 24 133 134 136 138 140 142 xpcco2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( <. ( ( y ( 2nd ` F ) z ) ` g ) , ( ( y ( 2nd ` G ) z ) ` g ) >. ( <. <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. , <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. >. ( comp ` T ) <. ( ( 1st ` F ) ` z ) , ( ( 1st ` G ) ` z ) >. ) <. ( ( x ( 2nd ` F ) y ) ` f ) , ( ( x ( 2nd ` G ) y ) ` f ) >. ) = <. ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) , ( ( ( y ( 2nd ` G ) z ) ` g ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` E ) ( ( 1st ` G ) ` z ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) >. )
144 126 143 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( ( y ( 2nd ` P ) z ) ` g ) ( <. ( ( 1st ` P ) ` x ) , ( ( 1st ` P ) ` y ) >. ( comp ` T ) ( ( 1st ` P ) ` z ) ) ( ( x ( 2nd ` P ) y ) ` f ) ) = <. ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) , ( ( ( y ( 2nd ` G ) z ) ` g ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` E ) ( ( 1st ` G ) ` z ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) >. )
145 114 118 144 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` P ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` P ) z ) ` g ) ( <. ( ( 1st ` P ) ` x ) , ( ( 1st ` P ) ` y ) >. ( comp ` T ) ( ( 1st ` P ) ` z ) ) ( ( x ( 2nd ` P ) y ) ` f ) ) )
146 5 19 6 20 21 22 23 24 27 32 44 50 81 101 145 isfuncd 
 |-  ( ph -> ( 1st ` P ) ( C Func T ) ( 2nd ` P ) )
147 df-br 
 |-  ( ( 1st ` P ) ( C Func T ) ( 2nd ` P ) <-> <. ( 1st ` P ) , ( 2nd ` P ) >. e. ( C Func T ) )
148 146 147 sylib 
 |-  ( ph -> <. ( 1st ` P ) , ( 2nd ` P ) >. e. ( C Func T ) )
149 16 148 eqeltrd 
 |-  ( ph -> P e. ( C Func T ) )