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 = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
	fvmpomptd.u	|- ( ph -> U e. B )
	fvmpomptd.v	|- ( ph -> V e. B )
	fvmpomptd.f	|- ( ph -> F e. ( U H V ) )
Assertion	fvmpomptd	|- ( ph -> ( ( U L V ) ` F ) = ( A ` F ) )

Proof

Step	Hyp	Ref	Expression
1		fnmpompt.l	|- L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
2		fvmpomptd.u	|- ( ph -> U e. B )
3		fvmpomptd.v	|- ( ph -> V e. B )
4		fvmpomptd.f	|- ( ph -> F e. ( U H V ) )
5	1 2 3	ovmpomptd	|- ( ph -> ( U L V ) = ( a e. ( U H V ) |-> ( A ` a ) ) )
6		simpr	|- ( ( ph /\ a = F ) -> a = F )
7	6	fveq2d	|- ( ( ph /\ a = F ) -> ( A ` a ) = ( A ` F ) )
8		fvexd	|- ( ph -> ( A ` F ) e. _V )
9	5 7 4 8	fvmptd	|- ( ph -> ( ( U L V ) ` F ) = ( A ` F ) )