Theorem fmpodg

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

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

Proof

Step	Hyp	Ref	Expression
1		fmpodg.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
2		fmpodg.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑆 )
3		fmpodg.3	⊢ ( 𝜑 → 𝑅 = ( 𝐴 × 𝐵 ) )
4	2	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑆 )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
6	5	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑆 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) : ( 𝐴 × 𝐵 ) ⟶ 𝑆 )
7	4 6	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) : ( 𝐴 × 𝐵 ) ⟶ 𝑆 )
8	1 3	feq12d	⊢ ( 𝜑 → ( 𝐹 : 𝑅 ⟶ 𝑆 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) : ( 𝐴 × 𝐵 ) ⟶ 𝑆 ) )
9	7 8	mpbird	⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ 𝑆 )