Metamath Proof Explorer

Theorem catcval

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

Ref Expression
Hypotheses catcval.c 
|- C = ( CatCat ` U )
catcval.u 
|- ( ph -> U e. V )
catcval.b 
|- ( ph -> B = ( U i^i Cat ) )
catcval.h 
|- ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )
catcval.o 
|- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
Assertion catcval 
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )

Proof

Step Hyp Ref Expression
1 catcval.c 
 |-  C = ( CatCat ` U )
2 catcval.u 
 |-  ( ph -> U e. V )
3 catcval.b 
 |-  ( ph -> B = ( U i^i Cat ) )
4 catcval.h 
 |-  ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )
5 catcval.o 
 |-  ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
6 df-catc 
 |-  CatCat = ( u e. _V |-> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )
7 vex 
 |-  u e. _V
8 7 inex1 
 |-  ( u i^i Cat ) e. _V
9 8 a1i 
 |-  ( ( ph /\ u = U ) -> ( u i^i Cat ) e. _V )
10 simpr 
 |-  ( ( ph /\ u = U ) -> u = U )
11 10 ineq1d 
 |-  ( ( ph /\ u = U ) -> ( u i^i Cat ) = ( U i^i Cat ) )
12 3 adantr 
 |-  ( ( ph /\ u = U ) -> B = ( U i^i Cat ) )
13 11 12 eqtr4d 
 |-  ( ( ph /\ u = U ) -> ( u i^i Cat ) = B )
14 simpr 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> b = B )
15 14 opeq2d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
16 eqidd 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( x Func y ) = ( x Func y ) )
17 14 14 16 mpoeq123dv 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( x e. b , y e. b |-> ( x Func y ) ) = ( x e. B , y e. B |-> ( x Func y ) ) )
18 4 ad2antrr 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> H = ( x e. B , y e. B |-> ( x Func y ) ) )
19 17 18 eqtr4d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( x e. b , y e. b |-> ( x Func y ) ) = H )
20 19 opeq2d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. = <. ( Hom ` ndx ) , H >. )
21 14 sqxpeqd 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
22 eqidd 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) = ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) )
23 21 14 22 mpoeq123dv 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( 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 ) ) ) )
24 5 ad2antrr 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
25 23 24 eqtr4d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) = .x. )
26 25 opeq2d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. = <. ( comp ` ndx ) , .x. >. )
27 15 20 26 tpeq123d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
28 9 13 27 csbied2 
 |-  ( ( ph /\ u = U ) -> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
29 2 elexd 
 |-  ( ph -> U e. _V )
30 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
31 30 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V )
32 6 28 29 31 fvmptd2 
 |-  ( ph -> ( CatCat ` U ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
33 1 32 eqtrid 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )