Metamath Proof Explorer


Theorem catccofval

Description: Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catcbas.c
|- C = ( CatCat ` U )
catcbas.b
|- B = ( Base ` C )
catcbas.u
|- ( ph -> U e. V )
catcco.o
|- .x. = ( comp ` C )
Assertion catccofval
|- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )

Proof

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