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	⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
	fvmpomptd.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	fvmpomptd.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	ovmpomptd	⊢ ( 𝜑 → ( 𝑈 𝐿 𝑉 ) = ( 𝑎 ∈ ( 𝑈 𝐻 𝑉 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnmpompt.l	⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
2		fvmpomptd.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
3		fvmpomptd.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
4	1	a1i	⊢ ( 𝜑 → 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ) )
5		simprl	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → 𝑢 = 𝑈 )
6		simprr	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → 𝑣 = 𝑉 )
7	5 6	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 𝑢 𝐻 𝑣 ) = ( 𝑈 𝐻 𝑉 ) )
8	7	mpteq1d	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) = ( 𝑎 ∈ ( 𝑈 𝐻 𝑉 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
9		ovex	⊢ ( 𝑈 𝐻 𝑉 ) ∈ V
10	9	mptex	⊢ ( 𝑎 ∈ ( 𝑈 𝐻 𝑉 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ∈ V
11	10	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑈 𝐻 𝑉 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ∈ V )
12	4 8 2 3 11	ovmpod	⊢ ( 𝜑 → ( 𝑈 𝐿 𝑉 ) = ( 𝑎 ∈ ( 𝑈 𝐻 𝑉 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )