Theorem mptelee

Description: A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by SN, 2-Feb-2026)

	Ref	Expression
Assertion	mptelee	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		elee	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
2		eqid	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) )
3	2	fmpt	⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ ↔ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) : ( 1 ... 𝑁 ) ⟶ ℝ )
4	1 3	bitr4di	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )