Metamath Proof Explorer

Theorem catcbas

Description: Set of objects of 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 )
Assertion catcbas 
|- ( ph -> B = ( U i^i Cat ) )

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 eqidd 
 |-  ( ph -> ( U i^i Cat ) = ( U i^i Cat ) )
5 eqidd 
 |-  ( ph -> ( x e. ( U i^i Cat ) , y e. ( U i^i Cat ) |-> ( x Func y ) ) = ( x e. ( U i^i Cat ) , y e. ( U i^i Cat ) |-> ( x Func y ) ) )
6 eqidd 
 |-  ( ph -> ( v e. ( ( U i^i Cat ) X. ( U i^i Cat ) ) , z e. ( U i^i Cat ) |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) = ( v e. ( ( U i^i Cat ) X. ( U i^i Cat ) ) , z e. ( U i^i Cat ) |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
7 1 3 4 5 6 catcval 
 |-  ( ph -> C = { <. ( Base ` ndx ) , ( U i^i Cat ) >. , <. ( Hom ` ndx ) , ( x e. ( U i^i Cat ) , y e. ( U i^i Cat ) |-> ( x Func y ) ) >. , <. ( comp ` ndx ) , ( v e. ( ( U i^i Cat ) X. ( U i^i Cat ) ) , z e. ( U i^i Cat ) |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )
8 catstr 
 |-  { <. ( Base ` ndx ) , ( U i^i Cat ) >. , <. ( Hom ` ndx ) , ( x e. ( U i^i Cat ) , y e. ( U i^i Cat ) |-> ( x Func y ) ) >. , <. ( comp ` ndx ) , ( v e. ( ( U i^i Cat ) X. ( U i^i Cat ) ) , z e. ( U i^i Cat ) |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } Struct <. 1 , ; 1 5 >.
9 baseid 
 |-  Base = Slot ( Base ` ndx )
10 snsstp1 
 |-  { <. ( Base ` ndx ) , ( U i^i Cat ) >. } C_ { <. ( Base ` ndx ) , ( U i^i Cat ) >. , <. ( Hom ` ndx ) , ( x e. ( U i^i Cat ) , y e. ( U i^i Cat ) |-> ( x Func y ) ) >. , <. ( comp ` ndx ) , ( v e. ( ( U i^i Cat ) X. ( U i^i Cat ) ) , z e. ( U i^i Cat ) |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. }
11 inex1g 
 |-  ( U e. V -> ( U i^i Cat ) e. _V )
12 3 11 syl 
 |-  ( ph -> ( U i^i Cat ) e. _V )
13 7 8 9 10 12 2 strfv3 
 |-  ( ph -> B = ( U i^i Cat ) )