Metamath Proof Explorer

Theorem estrchomfval

Description: Set of morphisms ("arrows") of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020)

		Ref	Expression
	Hypotheses	estrcbas.c	\|- C = ( ExtStrCat ` U )
		estrcbas.u	\|- ( ph -> U e. V )
		estrchomfval.h	\|- H = ( Hom ` C )
	Assertion	estrchomfval	\|- ( ph -> H = ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	\|- C = ( ExtStrCat ` U )
2		estrcbas.u	\|- ( ph -> U e. V )
3		estrchomfval.h	\|- H = ( Hom ` C )
4		eqidd	\|- ( ph -> ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
5		eqidd	\|- ( ph -> ( v e. ( U X. U ) , z e. U \|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) \|-> ( g o. f ) ) ) = ( v e. ( U X. U ) , z e. U \|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) \|-> ( g o. f ) ) ) )
6	1 2 4 5	estrcval	\|- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U \|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) \|-> ( g o. f ) ) ) >. } )
7		catstr	\|- { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U \|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 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 \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. } C_ { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U \|-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) \|-> ( g o. f ) ) ) >. }
10		mpoexga	\|- ( ( U e. V /\ U e. V ) -> ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V )
11	2 2 10	syl2anc	\|- ( ph -> ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V )
12	6 7 8 9 11 3	strfv3	\|- ( ph -> H = ( x e. U , y e. U \|-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )