Theorem elmaprd

Description: Deduction associated with elmapd . Reverse direction of elmapdd . (Contributed by Thierry Arnoux, 13-Oct-2025) Removed redundant hypotheses. (Revised by SN, 30-Aug-2026)

	Ref	Expression
Hypothesis	elmaprd.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) )
Assertion	elmaprd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elmaprd.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) )
2		elmapi	⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
3	1 2	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )