Theorem fconstmpo

Description: Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018)

	Ref	Expression
Assertion	fconstmpo	⊢ ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	⊢ ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 )
2		eqidd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐶 )
3	2	mpompt	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
4	1 3	eqtri	⊢ ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )