Metamath Proof Explorer

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 ∈ B , v ∈ B ⟼ a ∈ u H v ⟼ A ⁡ a
fvmpomptd.u ⊢ φ → U ∈ B
fvmpomptd.v ⊢ φ → V ∈ B
Assertion ovmpomptd ⊢ φ → U L V = a ∈ U H V ⟼ A ⁡ a

Proof

Step Hyp Ref Expression
1 fnmpompt.l ⊢ L = u ∈ B , v ∈ B ⟼ a ∈ u H v ⟼ A ⁡ a
2 fvmpomptd.u ⊢ φ → U ∈ B
3 fvmpomptd.v ⊢ φ → V ∈ B
4 1 a1i ⊢ φ → L = u ∈ B , v ∈ B ⟼ a ∈ u H v ⟼ A ⁡ a
5 simprl ⊢ φ ∧ u = U ∧ v = V → u = U
6 simprr ⊢ φ ∧ u = U ∧ v = V → v = V
7 5 6 oveq12d ⊢ φ ∧ u = U ∧ v = V → u H v = U H V
8 7 mpteq1d ⊢ φ ∧ u = U ∧ v = V → a ∈ u H v ⟼ A ⁡ a = a ∈ U H V ⟼ A ⁡ a
9 ovex ⊢ U H V ∈ V
10 9 mptex ⊢ a ∈ U H V ⟼ A ⁡ a ∈ V
11 10 a1i ⊢ φ → a ∈ U H V ⟼ A ⁡ a ∈ V
12 4 8 2 3 11 ovmpod ⊢ φ → U L V = a ∈ U H V ⟼ A ⁡ a