Metamath Proof Explorer

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 ⊢ N ∈ ℕ → k ∈ 1 … N ⟼ A F B ∈ 𝔼 ⁡ N ↔ ∀ k ∈ 1 … N A F B ∈ ℝ

Proof

Step Hyp Ref Expression
1 elee ⊢ N ∈ ℕ → k ∈ 1 … N ⟼ A F B ∈ 𝔼 ⁡ N ↔ k ∈ 1 … N ⟼ A F B : 1 … N ⟶ ℝ
2 eqid ⊢ k ∈ 1 … N ⟼ A F B = k ∈ 1 … N ⟼ A F B
3 2 fmpt ⊢ ∀ k ∈ 1 … N A F B ∈ ℝ ↔ k ∈ 1 … N ⟼ A F B : 1 … N ⟶ ℝ
4 1 3 bitr4di ⊢ N ∈ ℕ → k ∈ 1 … N ⟼ A F B ∈ 𝔼 ⁡ N ↔ ∀ k ∈ 1 … N A F B ∈ ℝ