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	|- L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
Assertion	fnmpompt	|- L Fn ( B X. B )

Proof

Step	Hyp	Ref	Expression
1		fnmpompt.l	|- L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
2		ovex	|- ( u H v ) e. _V
3	2	mptex	|- ( a e. ( u H v ) |-> ( A ` a ) ) e. _V
4	1 3	fnmpoi	|- L Fn ( B X. B )