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=\mathrm{RngCatALTV}\left(U\right)$$
	rngchomffvalALTV.b	$$⊢B={\mathrm{Base}}_C$$
	rngchomffvalALTV.u	$$⊢\phi \to U\in V$$
	rngchomffvalALTV.h	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
Assertion	rngchomffvalALTV	$$⊢\phi \to F=\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngchomffvalALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
2		rngchomffvalALTV.b	$$⊢B={\mathrm{Base}}_C$$
3		rngchomffvalALTV.u	$$⊢\phi \to U\in V$$
4		rngchomffvalALTV.h	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
5		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
6	1 2 3 5	rngchomfvalALTV	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)$$
7		eqid	$$⊢\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)=\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)$$
8		ovex	$$⊢x\mathrm{RngHom}y\in \mathrm{V}$$
9	7 8	fnmpoi	$$⊢\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)Fn\left(B\times B\right)$$
10		fneq1	$$⊢\mathrm{Hom}\left(C\right)=\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)\to \left(\mathrm{Hom}\left(C\right)Fn\left(B\times B\right)\leftrightarrow \left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)Fn\left(B\times B\right)\right)$$
11	9 10	mpbiri	$$⊢\mathrm{Hom}\left(C\right)=\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)\to \mathrm{Hom}\left(C\right)Fn\left(B\times B\right)$$
12	4 2 5	fnhomeqhomf	$$⊢\mathrm{Hom}\left(C\right)Fn\left(B\times B\right)\to F=\mathrm{Hom}\left(C\right)$$
13	6 11 12	3syl	$$⊢\phi \to F=\mathrm{Hom}\left(C\right)$$
14	13 6	eqtrd	$$⊢\phi \to F=\left(x\in B,y\in B⟼x\mathrm{RngHom}y\right)$$