Theorem fvmpomptd

Description: At an element of its inner domain, an iterated maps-to function has the value of its body. The operation H is arbitrary; evaluation on a morphism in a hom-set is one application. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fnmpompt.l	$$⊢L=\left(u\in B,v\in B⟼\left(a\in \left(uHv\right)⟼A\left(a\right)\right)\right)$$
	fvmpomptd.u	$$⊢\phi \to U\in B$$
	fvmpomptd.v	$$⊢\phi \to V\in B$$
	fvmpomptd.f	$$⊢\phi \to F\in \left(UHV\right)$$
Assertion	fvmpomptd	$$⊢\phi \to \left(ULV\right)\left(F\right)=A\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnmpompt.l	$$⊢L=\left(u\in B,v\in B⟼\left(a\in \left(uHv\right)⟼A\left(a\right)\right)\right)$$
2		fvmpomptd.u	$$⊢\phi \to U\in B$$
3		fvmpomptd.v	$$⊢\phi \to V\in B$$
4		fvmpomptd.f	$$⊢\phi \to F\in \left(UHV\right)$$
5	1 2 3	ovmpomptd	$$⊢\phi \to ULV=\left(a\in \left(UHV\right)⟼A\left(a\right)\right)$$
6		simpr	$$⊢\left(\phi \wedge a=F\right)\to a=F$$
7	6	fveq2d	$$⊢\left(\phi \wedge a=F\right)\to A\left(a\right)=A\left(F\right)$$
8		fvexd	$$⊢\phi \to A\left(F\right)\in \mathrm{V}$$
9	5 7 4 8	fvmptd	$$⊢\phi \to \left(ULV\right)\left(F\right)=A\left(F\right)$$