Theorem fnmpompt

Description: Characterization of the outer domain of a chained maps-to expression. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypothesis	fnmpompt.l	⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
Assertion	fnmpompt	⊢ 𝐿 Fn ( 𝐵 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fnmpompt.l	⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
2		ovex	⊢ ( 𝑢 𝐻 𝑣 ) ∈ V
3	2	mptex	⊢ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ∈ V
4	1 3	fnmpoi	⊢ 𝐿 Fn ( 𝐵 × 𝐵 )