Theorem ovmpomptd

Description: The outer value of an iterated maps-to function is the corresponding inner maps-to function. (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 )
Assertion	ovmpomptd	|- ( ph -> ( U L V ) = ( a e. ( U H V ) |-> ( A ` a ) ) )

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	1	a1i	|- ( ph -> L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) ) )
5		simprl	|- ( ( ph /\ ( u = U /\ v = V ) ) -> u = U )
6		simprr	|- ( ( ph /\ ( u = U /\ v = V ) ) -> v = V )
7	5 6	oveq12d	|- ( ( ph /\ ( u = U /\ v = V ) ) -> ( u H v ) = ( U H V ) )
8	7	mpteq1d	|- ( ( ph /\ ( u = U /\ v = V ) ) -> ( a e. ( u H v ) |-> ( A ` a ) ) = ( a e. ( U H V ) |-> ( A ` a ) ) )
9		ovex	|- ( U H V ) e. _V
10	9	mptex	|- ( a e. ( U H V ) |-> ( A ` a ) ) e. _V
11	10	a1i	|- ( ph -> ( a e. ( U H V ) |-> ( A ` a ) ) e. _V )
12	4 8 2 3 11	ovmpod	|- ( ph -> ( U L V ) = ( a e. ( U H V ) |-> ( A ` a ) ) )