Theorem fconst

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Hypothesis	fconst.1	⊢ 𝐵 ∈ V
Assertion	fconst	⊢ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		fconst.1	⊢ 𝐵 ∈ V
2		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	1 2	fnmpti	⊢ ( 𝐴 × { 𝐵 } ) Fn 𝐴
4		rnxpss	⊢ ran ( 𝐴 × { 𝐵 } ) ⊆ { 𝐵 }
5		df-f	⊢ ( ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ↔ ( ( 𝐴 × { 𝐵 } ) Fn 𝐴 ∧ ran ( 𝐴 × { 𝐵 } ) ⊆ { 𝐵 } ) )
6	3 4 5	mpbir2an	⊢ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 }