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