Metamath Proof Explorer

Theorem 1stfcl

Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfcl.t 
|- T = ( C Xc. D )
1stfcl.c 
|- ( ph -> C e. Cat )
1stfcl.d 
|- ( ph -> D e. Cat )
1stfcl.p 
|- P = ( C 1stF D )
Assertion 1stfcl 
|- ( ph -> P e. ( T Func C ) )

Proof

Step Hyp Ref Expression
1 1stfcl.t 
 |-  T = ( C Xc. D )
2 1stfcl.c 
 |-  ( ph -> C e. Cat )
3 1stfcl.d 
 |-  ( ph -> D e. Cat )
4 1stfcl.p 
 |-  P = ( C 1stF D )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 1 5 6 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` T )
8 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
9 1 7 8 2 3 4 1stfval 
 |-  ( ph -> P = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) >. )
10 fo1st 
 |-  1st : _V -onto-> _V
11 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
12 10 11 ax-mp 
 |-  Fun 1st
13 fvex 
 |-  ( Base ` C ) e. _V
14 fvex 
 |-  ( Base ` D ) e. _V
15 13 14 xpex 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) e. _V
16 resfunexg 
 |-  ( ( Fun 1st /\ ( ( Base ` C ) X. ( Base ` D ) ) e. _V ) -> ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) e. _V )
17 12 15 16 mp2an 
 |-  ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) e. _V
18 15 15 mpoex 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) e. _V
19 17 18 op2ndd 
 |-  ( P = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) >. -> ( 2nd ` P ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) )
20 9 19 syl 
 |-  ( ph -> ( 2nd ` P ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) )
21 20 opeq2d 
 |-  ( ph -> <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` P ) >. = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) >. )
22 9 21 eqtr4d 
 |-  ( ph -> P = <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` P ) >. )
23 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
24 eqid 
 |-  ( Id ` T ) = ( Id ` T )
25 eqid 
 |-  ( Id ` C ) = ( Id ` C )
26 eqid 
 |-  ( comp ` T ) = ( comp ` T )
27 eqid 
 |-  ( comp ` C ) = ( comp ` C )
28 1 2 3 xpccat 
 |-  ( ph -> T e. Cat )
29 f1stres 
 |-  ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` C )
30 29 a1i 
 |-  ( ph -> ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` C ) )
31 eqid 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) )
32 ovex 
 |-  ( x ( Hom ` T ) y ) e. _V
33 resfunexg 
 |-  ( ( Fun 1st /\ ( x ( Hom ` T ) y ) e. _V ) -> ( 1st |` ( x ( Hom ` T ) y ) ) e. _V )
34 12 32 33 mp2an 
 |-  ( 1st |` ( x ( Hom ` T ) y ) ) e. _V
35 31 34 fnmpoi 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) )
36 20 fneq1d 
 |-  ( ph -> ( ( 2nd ` P ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) <-> ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 1st |` ( x ( Hom ` T ) y ) ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) ) )
37 35 36 mpbiri 
 |-  ( ph -> ( 2nd ` P ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) )
38 f1stres 
 |-  ( 1st |` ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) )
39 2 adantr 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> C e. Cat )
40 3 adantr 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> D e. Cat )
41 simprl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` D ) ) )
42 simprr 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> y e. ( ( Base ` C ) X. ( Base ` D ) ) )
43 1 7 8 39 40 4 41 42 1stf2 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` P ) y ) = ( 1st |` ( x ( Hom ` T ) y ) ) )
44 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
45 1 7 23 44 8 41 42 xpchom 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( Hom ` T ) y ) = ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) )
46 45 reseq2d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( 1st |` ( x ( Hom ` T ) y ) ) = ( 1st |` ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) ) )
47 43 46 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` P ) y ) = ( 1st |` ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) ) )
48 47 feq1d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( x ( 2nd ` P ) y ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) <-> ( 1st |` ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) ) )
49 38 48 mpbiri 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` P ) y ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) )
50 fvres 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 1st ` x ) )
51 50 ad2antrl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 1st ` x ) )
52 fvres 
 |-  ( y e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) = ( 1st ` y ) )
53 52 ad2antll 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) = ( 1st ` y ) )
54 51 53 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ( Hom ` C ) ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) ) = ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) )
55 45 54 feq23d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( x ( 2nd ` P ) y ) : ( x ( Hom ` T ) y ) --> ( ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ( Hom ` C ) ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) ) <-> ( x ( 2nd ` P ) y ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) ) )
56 49 55 mpbird 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` P ) y ) : ( x ( Hom ` T ) y ) --> ( ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ( Hom ` C ) ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) ) )
57 28 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> T e. Cat )
58 simpr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` D ) ) )
59 7 8 24 57 58 catidcl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( Id ` T ) ` x ) e. ( x ( Hom ` T ) x ) )
60 59 fvresd 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( 1st |` ( x ( Hom ` T ) x ) ) ` ( ( Id ` T ) ` x ) ) = ( 1st ` ( ( Id ` T ) ` x ) ) )
61 1st2nd2 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
62 61 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
63 62 fveq2d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( Id ` T ) ` x ) = ( ( Id ` T ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
64 2 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> C e. Cat )
65 3 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> D e. Cat )
66 eqid 
 |-  ( Id ` D ) = ( Id ` D )
67 xp1st 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 1st ` x ) e. ( Base ` C ) )
68 67 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( 1st ` x ) e. ( Base ` C ) )
69 xp2nd 
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 2nd ` x ) e. ( Base ` D ) )
70 69 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( 2nd ` x ) e. ( Base ` D ) )
71 1 64 65 5 6 25 66 24 68 70 xpcid 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( Id ` T ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) = <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` D ) ` ( 2nd ` x ) ) >. )
72 63 71 eqtrd 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( Id ` T ) ` x ) = <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` D ) ` ( 2nd ` x ) ) >. )
73 fvex 
 |-  ( ( Id ` C ) ` ( 1st ` x ) ) e. _V
74 fvex 
 |-  ( ( Id ` D ) ` ( 2nd ` x ) ) e. _V
75 73 74 op1std 
 |-  ( ( ( Id ` T ) ` x ) = <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` D ) ` ( 2nd ` x ) ) >. -> ( 1st ` ( ( Id ` T ) ` x ) ) = ( ( Id ` C ) ` ( 1st ` x ) ) )
76 72 75 syl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( 1st ` ( ( Id ` T ) ` x ) ) = ( ( Id ` C ) ` ( 1st ` x ) ) )
77 60 76 eqtrd 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( 1st |` ( x ( Hom ` T ) x ) ) ` ( ( Id ` T ) ` x ) ) = ( ( Id ` C ) ` ( 1st ` x ) ) )
78 1 7 8 64 65 4 58 58 1stf2 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( x ( 2nd ` P ) x ) = ( 1st |` ( x ( Hom ` T ) x ) ) )
79 78 fveq1d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( x ( 2nd ` P ) x ) ` ( ( Id ` T ) ` x ) ) = ( ( 1st |` ( x ( Hom ` T ) x ) ) ` ( ( Id ` T ) ` x ) ) )
80 50 adantl 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 1st ` x ) )
81 80 fveq2d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( Id ` C ) ` ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ) = ( ( Id ` C ) ` ( 1st ` x ) ) )
82 77 79 81 3eqtr4d 
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( x ( 2nd ` P ) x ) ` ( ( Id ` T ) ` x ) ) = ( ( Id ` C ) ` ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ) )
83 28 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> T e. Cat )
84 simp21 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> x e. ( ( Base ` C ) X. ( Base ` D ) ) )
85 simp22 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> y e. ( ( Base ` C ) X. ( Base ` D ) ) )
86 simp23 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> z e. ( ( Base ` C ) X. ( Base ` D ) ) )
87 simp3l 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> f e. ( x ( Hom ` T ) y ) )
88 simp3r 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> g e. ( y ( Hom ` T ) z ) )
89 7 8 26 83 84 85 86 87 88 catcocl 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( g ( <. x , y >. ( comp ` T ) z ) f ) e. ( x ( Hom ` T ) z ) )
90 89 fvresd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( x ( Hom ` T ) z ) ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( 1st ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) )
91 1 7 8 26 84 85 86 87 88 27 xpcco1st 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( 1st ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( 1st ` g ) ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` z ) ) ( 1st ` f ) ) )
92 90 91 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( x ( Hom ` T ) z ) ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( 1st ` g ) ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` z ) ) ( 1st ` f ) ) )
93 2 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> C e. Cat )
94 3 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> D e. Cat )
95 1 7 8 93 94 4 84 86 1stf2 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( x ( 2nd ` P ) z ) = ( 1st |` ( x ( Hom ` T ) z ) ) )
96 95 fveq1d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( x ( 2nd ` P ) z ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( 1st |` ( x ( Hom ` T ) z ) ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) )
97 84 fvresd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 1st ` x ) )
98 85 fvresd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) = ( 1st ` y ) )
99 97 98 opeq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> <. ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. = <. ( 1st ` x ) , ( 1st ` y ) >. )
100 86 fvresd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) = ( 1st ` z ) )
101 99 100 oveq12d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( <. ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. ( comp ` C ) ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) ) = ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` z ) ) )
102 1 7 8 93 94 4 85 86 1stf2 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( y ( 2nd ` P ) z ) = ( 1st |` ( y ( Hom ` T ) z ) ) )
103 102 fveq1d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( y ( 2nd ` P ) z ) ` g ) = ( ( 1st |` ( y ( Hom ` T ) z ) ) ` g ) )
104 88 fvresd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( y ( Hom ` T ) z ) ) ` g ) = ( 1st ` g ) )
105 103 104 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( y ( 2nd ` P ) z ) ` g ) = ( 1st ` g ) )
106 1 7 8 93 94 4 84 85 1stf2 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( x ( 2nd ` P ) y ) = ( 1st |` ( x ( Hom ` T ) y ) ) )
107 106 fveq1d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( x ( 2nd ` P ) y ) ` f ) = ( ( 1st |` ( x ( Hom ` T ) y ) ) ` f ) )
108 87 fvresd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( 1st |` ( x ( Hom ` T ) y ) ) ` f ) = ( 1st ` f ) )
109 107 108 eqtrd 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( x ( 2nd ` P ) y ) ` f ) = ( 1st ` f ) )
110 101 105 109 oveq123d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( ( y ( 2nd ` P ) z ) ` g ) ( <. ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. ( comp ` C ) ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) ) ( ( x ( 2nd ` P ) y ) ` f ) ) = ( ( 1st ` g ) ( <. ( 1st ` x ) , ( 1st ` y ) >. ( comp ` C ) ( 1st ` z ) ) ( 1st ` f ) ) )
111 92 96 110 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) /\ z e. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` T ) y ) /\ g e. ( y ( Hom ` T ) z ) ) ) -> ( ( x ( 2nd ` P ) z ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( ( y ( 2nd ` P ) z ) ` g ) ( <. ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. ( comp ` C ) ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) ) ( ( x ( 2nd ` P ) y ) ` f ) ) )
112 7 5 8 23 24 25 26 27 28 2 30 37 56 82 111 isfuncd 
 |-  ( ph -> ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ( T Func C ) ( 2nd ` P ) )
113 df-br 
 |-  ( ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) ( T Func C ) ( 2nd ` P ) <-> <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` P ) >. e. ( T Func C ) )
114 112 113 sylib 
 |-  ( ph -> <. ( 1st |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` P ) >. e. ( T Func C ) )
115 22 114 eqeltrd 
 |-  ( ph -> P e. ( T Func C ) )