Step |
Hyp |
Ref |
Expression |
1 |
|
catcbas.c |
|- C = ( CatCat ` U ) |
2 |
|
catcbas.b |
|- B = ( Base ` C ) |
3 |
|
catcbas.u |
|- ( ph -> U e. V ) |
4 |
|
catcco.o |
|- .x. = ( comp ` C ) |
5 |
1 2 3
|
catcbas |
|- ( ph -> B = ( U i^i Cat ) ) |
6 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
7 |
1 2 3 6
|
catchomfval |
|- ( ph -> ( Hom ` C ) = ( x e. B , y e. B |-> ( x Func y ) ) ) |
8 |
|
eqidd |
|- ( ph -> ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) ) |
9 |
1 3 5 7 8
|
catcval |
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } ) |
10 |
9
|
fveq2d |
|- ( ph -> ( comp ` C ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } ) ) |
11 |
2
|
fvexi |
|- B e. _V |
12 |
11 11
|
xpex |
|- ( B X. B ) e. _V |
13 |
12 11
|
mpoex |
|- ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) e. _V |
14 |
|
catstr |
|- { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } Struct <. 1 , ; 1 5 >. |
15 |
|
ccoid |
|- comp = Slot ( comp ` ndx ) |
16 |
|
snsstp3 |
|- { <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } |
17 |
14 15 16
|
strfv |
|- ( ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) e. _V -> ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } ) ) |
18 |
13 17
|
ax-mp |
|- ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } ) |
19 |
10 4 18
|
3eqtr4g |
|- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) ) |