Theorem constmap

Description: A constant (represented without dummy variables) is an element of a function set.

Note: In the following development, we will be quite often quantifying over functions and points in N-dimensional space (which are equivalent to functions from an "index set"). Many of the following theorems exist to transfer standard facts about functions to elements of function sets. (Contributed by Stefan O'Rear, 30-Aug-2014) (Revised by Stefan O'Rear, 5-May-2015)

	Ref	Expression
Hypotheses	constmap.1	⊢ 𝐴 ∈ V
	constmap.3	⊢ 𝐶 ∈ V
Assertion	constmap	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) ∈ ( 𝐶 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		constmap.1	⊢ 𝐴 ∈ V
2		constmap.3	⊢ 𝐶 ∈ V
3		fconst6g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶 )
4	2 1	elmap	⊢ ( ( 𝐴 × { 𝐵 } ) ∈ ( 𝐶 ↑m 𝐴 ) ↔ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ 𝐶 )
5	3 4	sylibr	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) ∈ ( 𝐶 ↑m 𝐴 ) )