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 ) ) |