Description: At an element of its inner domain, an iterated maps-to function has the value of its body. The operation H is arbitrary; evaluation on a morphism in a hom-set is one application. (Contributed by Zhi Wang, 14-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fnmpompt.l | ⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ) | |
| fvmpomptd.u | ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 ) | ||
| fvmpomptd.v | ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 ) | ||
| fvmpomptd.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ) | ||
| Assertion | fvmpomptd | ⊢ ( 𝜑 → ( ( 𝑈 𝐿 𝑉 ) ‘ 𝐹 ) = ( 𝐴 ‘ 𝐹 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fnmpompt.l | ⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ) | |
| 2 | fvmpomptd.u | ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 ) | |
| 3 | fvmpomptd.v | ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 ) | |
| 4 | fvmpomptd.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ) | |
| 5 | 1 2 3 | ovmpomptd | ⊢ ( 𝜑 → ( 𝑈 𝐿 𝑉 ) = ( 𝑎 ∈ ( 𝑈 𝐻 𝑉 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ) |
| 6 | simpr | ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐹 ) → 𝑎 = 𝐹 ) | |
| 7 | 6 | fveq2d | ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐹 ) → ( 𝐴 ‘ 𝑎 ) = ( 𝐴 ‘ 𝐹 ) ) |
| 8 | fvexd | ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ V ) | |
| 9 | 5 7 4 8 | fvmptd | ⊢ ( 𝜑 → ( ( 𝑈 𝐿 𝑉 ) ‘ 𝐹 ) = ( 𝐴 ‘ 𝐹 ) ) |