Theorem fmpod

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fmpodg.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
	fmpodg.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑆 )
Assertion	fmpod	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fmpodg.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
2		fmpodg.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑆 )
3		eqidd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) )
4	1 2 3	fmpodg	⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝑆 )