Metamath Proof Explorer


Theorem 2ndfcl

Description: The second projection functor is a functor onto the right 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 )
2ndfcl.p
|- Q = ( C 2ndF D )
Assertion 2ndfcl
|- ( ph -> Q e. ( T Func D ) )

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 2ndfcl.p
 |-  Q = ( C 2ndF 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 2ndfval
 |-  ( ph -> Q = <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) >. )
10 fo2nd
 |-  2nd : _V -onto-> _V
11 fofun
 |-  ( 2nd : _V -onto-> _V -> Fun 2nd )
12 10 11 ax-mp
 |-  Fun 2nd
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 2nd /\ ( ( Base ` C ) X. ( Base ` D ) ) e. _V ) -> ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) e. _V )
17 12 15 16 mp2an
 |-  ( 2nd |` ( ( 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 ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) e. _V
19 17 18 op2ndd
 |-  ( Q = <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) >. -> ( 2nd ` Q ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) )
20 9 19 syl
 |-  ( ph -> ( 2nd ` Q ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) )
21 20 opeq2d
 |-  ( ph -> <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` Q ) >. = <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) >. )
22 9 21 eqtr4d
 |-  ( ph -> Q = <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` Q ) >. )
23 eqid
 |-  ( Hom ` D ) = ( Hom ` D )
24 eqid
 |-  ( Id ` T ) = ( Id ` T )
25 eqid
 |-  ( Id ` D ) = ( Id ` D )
26 eqid
 |-  ( comp ` T ) = ( comp ` T )
27 eqid
 |-  ( comp ` D ) = ( comp ` D )
28 1 2 3 xpccat
 |-  ( ph -> T e. Cat )
29 f2ndres
 |-  ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` D )
30 29 a1i
 |-  ( ph -> ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` D ) )
31 eqid
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) )
32 ovex
 |-  ( x ( Hom ` T ) y ) e. _V
33 resfunexg
 |-  ( ( Fun 2nd /\ ( x ( Hom ` T ) y ) e. _V ) -> ( 2nd |` ( x ( Hom ` T ) y ) ) e. _V )
34 12 32 33 mp2an
 |-  ( 2nd |` ( x ( Hom ` T ) y ) ) e. _V
35 31 34 fnmpoi
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) )
36 20 fneq1d
 |-  ( ph -> ( ( 2nd ` Q ) 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 ) ) |-> ( 2nd |` ( x ( Hom ` T ) y ) ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) ) )
37 35 36 mpbiri
 |-  ( ph -> ( 2nd ` Q ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) )
38 f2ndres
 |-  ( 2nd |` ( ( ( 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 ) ) ) --> ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` 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 2ndf2
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` Q ) y ) = ( 2nd |` ( x ( Hom ` T ) y ) ) )
44 eqid
 |-  ( Hom ` C ) = ( Hom ` C )
45 1 7 44 23 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 ) ) ) ) -> ( 2nd |` ( x ( Hom ` T ) y ) ) = ( 2nd |` ( ( ( 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 ` Q ) y ) = ( 2nd |` ( ( ( 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 ` Q ) y ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) <-> ( 2nd |` ( ( ( 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 ) ) ) --> ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) )
49 38 48 mpbiri
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` Q ) y ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) )
50 fvres
 |-  ( x e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 2nd ` x ) )
51 50 ad2antrl
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 2nd ` x ) )
52 fvres
 |-  ( y e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) = ( 2nd ` y ) )
53 52 ad2antll
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) = ( 2nd ` y ) )
54 51 53 oveq12d
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ( Hom ` D ) ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) ) = ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) )
55 45 54 feq23d
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( x ( 2nd ` Q ) y ) : ( x ( Hom ` T ) y ) --> ( ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ( Hom ` D ) ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) ) <-> ( x ( 2nd ` Q ) y ) : ( ( ( 1st ` x ) ( Hom ` C ) ( 1st ` y ) ) X. ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) --> ( ( 2nd ` x ) ( Hom ` D ) ( 2nd ` y ) ) ) )
56 49 55 mpbird
 |-  ( ( ph /\ ( x e. ( ( Base ` C ) X. ( Base ` D ) ) /\ y e. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( x ( 2nd ` Q ) y ) : ( x ( Hom ` T ) y ) --> ( ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ( Hom ` D ) ( ( 2nd |` ( ( 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 ) ) ) -> ( ( 2nd |` ( x ( Hom ` T ) x ) ) ` ( ( Id ` T ) ` x ) ) = ( 2nd ` ( ( 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 ` C ) = ( Id ` C )
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 66 25 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 op2ndd
 |-  ( ( ( Id ` T ) ` x ) = <. ( ( Id ` C ) ` ( 1st ` x ) ) , ( ( Id ` D ) ` ( 2nd ` x ) ) >. -> ( 2nd ` ( ( Id ` T ) ` x ) ) = ( ( Id ` D ) ` ( 2nd ` x ) ) )
76 72 75 syl
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( 2nd ` ( ( Id ` T ) ` x ) ) = ( ( Id ` D ) ` ( 2nd ` x ) ) )
77 60 76 eqtrd
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( 2nd |` ( x ( Hom ` T ) x ) ) ` ( ( Id ` T ) ` x ) ) = ( ( Id ` D ) ` ( 2nd ` x ) ) )
78 1 7 8 64 65 4 58 58 2ndf2
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( x ( 2nd ` Q ) x ) = ( 2nd |` ( x ( Hom ` T ) x ) ) )
79 78 fveq1d
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( x ( 2nd ` Q ) x ) ` ( ( Id ` T ) ` x ) ) = ( ( 2nd |` ( x ( Hom ` T ) x ) ) ` ( ( Id ` T ) ` x ) ) )
80 50 adantl
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 2nd ` x ) )
81 80 fveq2d
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( Id ` D ) ` ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) ) = ( ( Id ` D ) ` ( 2nd ` x ) ) )
82 77 79 81 3eqtr4d
 |-  ( ( ph /\ x e. ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( x ( 2nd ` Q ) x ) ` ( ( Id ` T ) ` x ) ) = ( ( Id ` D ) ` ( ( 2nd |` ( ( 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 ) ) ) -> ( ( 2nd |` ( x ( Hom ` T ) z ) ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( 2nd ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) )
91 1 7 8 26 84 85 86 87 88 27 xpcco2nd
 |-  ( ( 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 ) ) ) -> ( 2nd ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` D ) ( 2nd ` z ) ) ( 2nd ` 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 ) ) ) -> ( ( 2nd |` ( x ( Hom ` T ) z ) ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` D ) ( 2nd ` z ) ) ( 2nd ` 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 2ndf2
 |-  ( ( 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 ` Q ) z ) = ( 2nd |` ( 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 ` Q ) z ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( 2nd |` ( 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 ) ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) = ( 2nd ` 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 ) ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) = ( 2nd ` 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 ) ) ) -> <. ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. = <. ( 2nd ` x ) , ( 2nd ` 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 ) ) ) -> ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) = ( 2nd ` 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 ) ) ) -> ( <. ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. ( comp ` D ) ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) ) = ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` D ) ( 2nd ` z ) ) )
102 1 7 8 93 94 4 85 86 2ndf2
 |-  ( ( 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 ` Q ) z ) = ( 2nd |` ( 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 ` Q ) z ) ` g ) = ( ( 2nd |` ( 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 ) ) ) -> ( ( 2nd |` ( y ( Hom ` T ) z ) ) ` g ) = ( 2nd ` 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 ` Q ) z ) ` g ) = ( 2nd ` g ) )
106 1 7 8 93 94 4 84 85 2ndf2
 |-  ( ( 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 ` Q ) y ) = ( 2nd |` ( 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 ` Q ) y ) ` f ) = ( ( 2nd |` ( 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 ) ) ) -> ( ( 2nd |` ( x ( Hom ` T ) y ) ) ` f ) = ( 2nd ` 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 ` Q ) y ) ` f ) = ( 2nd ` 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 ` Q ) z ) ` g ) ( <. ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. ( comp ` D ) ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) ) ( ( x ( 2nd ` Q ) y ) ` f ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` x ) , ( 2nd ` y ) >. ( comp ` D ) ( 2nd ` z ) ) ( 2nd ` 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 ` Q ) z ) ` ( g ( <. x , y >. ( comp ` T ) z ) f ) ) = ( ( ( y ( 2nd ` Q ) z ) ` g ) ( <. ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` x ) , ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` y ) >. ( comp ` D ) ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ` z ) ) ( ( x ( 2nd ` Q ) y ) ` f ) ) )
112 7 6 8 23 24 25 26 27 28 3 30 37 56 82 111 isfuncd
 |-  ( ph -> ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ( T Func D ) ( 2nd ` Q ) )
113 df-br
 |-  ( ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) ( T Func D ) ( 2nd ` Q ) <-> <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` Q ) >. e. ( T Func D ) )
114 112 113 sylib
 |-  ( ph -> <. ( 2nd |` ( ( Base ` C ) X. ( Base ` D ) ) ) , ( 2nd ` Q ) >. e. ( T Func D ) )
115 22 114 eqeltrd
 |-  ( ph -> Q e. ( T Func D ) )