Theorem rngchomffvalALTV

Description: The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngchomffvalALTV.c	|- C = ( RngCatALTV ` U )
	rngchomffvalALTV.b	|- B = ( Base ` C )
	rngchomffvalALTV.u	|- ( ph -> U e. V )
	rngchomffvalALTV.h	|- F = ( Homf ` C )
Assertion	rngchomffvalALTV	|- ( ph -> F = ( x e. B , y e. B |-> ( x RngHomo y ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngchomffvalALTV.c	|- C = ( RngCatALTV ` U )
2		rngchomffvalALTV.b	|- B = ( Base ` C )
3		rngchomffvalALTV.u	|- ( ph -> U e. V )
4		rngchomffvalALTV.h	|- F = ( Homf ` C )
5		eqid	|- ( Hom ` C ) = ( Hom ` C )
6	1 2 3 5	rngchomfvalALTV	|- ( ph -> ( Hom ` C ) = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
7		eqid	|- ( x e. B , y e. B |-> ( x RngHomo y ) ) = ( x e. B , y e. B |-> ( x RngHomo y ) )
8		ovex	|- ( x RngHomo y ) e. _V
9	7 8	fnmpoi	|- ( x e. B , y e. B |-> ( x RngHomo y ) ) Fn ( B X. B )
10		fneq1	|- ( ( Hom ` C ) = ( x e. B , y e. B |-> ( x RngHomo y ) ) -> ( ( Hom ` C ) Fn ( B X. B ) <-> ( x e. B , y e. B |-> ( x RngHomo y ) ) Fn ( B X. B ) ) )
11	9 10	mpbiri	|- ( ( Hom ` C ) = ( x e. B , y e. B |-> ( x RngHomo y ) ) -> ( Hom ` C ) Fn ( B X. B ) )
12	4 2 5	fnhomeqhomf	|- ( ( Hom ` C ) Fn ( B X. B ) -> F = ( Hom ` C ) )
13	6 11 12	3syl	|- ( ph -> F = ( Hom ` C ) )
14	13 6	eqtrd	|- ( ph -> F = ( x e. B , y e. B |-> ( x RngHomo y ) ) )