Metamath Proof Explorer


Theorem setchomfval

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

Ref Expression
Hypotheses setcbas.c
|- C = ( SetCat ` U )
setcbas.u
|- ( ph -> U e. V )
setchomfval.h
|- H = ( Hom ` C )
Assertion setchomfval
|- ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )

Proof

Step Hyp Ref Expression
1 setcbas.c
 |-  C = ( SetCat ` U )
2 setcbas.u
 |-  ( ph -> U e. V )
3 setchomfval.h
 |-  H = ( Hom ` C )
4 eqidd
 |-  ( ph -> ( x e. U , y e. U |-> ( y ^m x ) ) = ( x e. U , y e. U |-> ( y ^m x ) ) )
5 eqidd
 |-  ( ph -> ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )
6 1 2 4 5 setcval
 |-  ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } )
7 catstr
 |-  { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } Struct <. 1 , ; 1 5 >.
8 homid
 |-  Hom = Slot ( Hom ` ndx )
9 snsstp2
 |-  { <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. } C_ { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. }
10 mpoexga
 |-  ( ( U e. V /\ U e. V ) -> ( x e. U , y e. U |-> ( y ^m x ) ) e. _V )
11 2 2 10 syl2anc
 |-  ( ph -> ( x e. U , y e. U |-> ( y ^m x ) ) e. _V )
12 6 7 8 9 11 3 strfv3
 |-  ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )