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)

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 ovex ⊢ A F B ∈ V
3 eqid ⊢ k ∈ 1 … N ⟼ A F B = k ∈ 1 … N ⟼ A F B
4 2 3 fnmpti ⊢ k ∈ 1 … N ⟼ A F B Fn 1 … N
5 df-f ⊢ k ∈ 1 … N ⟼ A F B : 1 … N ⟶ ℝ ↔ k ∈ 1 … N ⟼ A F B Fn 1 … N ∧ ran ⁡ k ∈ 1 … N ⟼ A F B ⊆ ℝ
6 4 5 mpbiran ⊢ k ∈ 1 … N ⟼ A F B : 1 … N ⟶ ℝ ↔ ran ⁡ k ∈ 1 … N ⟼ A F B ⊆ ℝ
7 3 rnmpt ⊢ ran ⁡ k ∈ 1 … N ⟼ A F B = a | ∃ k ∈ 1 … N a = A F B
8 7 sseq1i ⊢ ran ⁡ k ∈ 1 … N ⟼ A F B ⊆ ℝ ↔ a | ∃ k ∈ 1 … N a = A F B ⊆ ℝ
9 abss ⊢ a | ∃ k ∈ 1 … N a = A F B ⊆ ℝ ↔ ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
10 nfre1 ⊢ Ⅎ k ∃ k ∈ 1 … N a = A F B
11 nfv ⊢ Ⅎ k a ∈ ℝ
12 10 11 nfim ⊢ Ⅎ k ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
13 12 nfal ⊢ Ⅎ k ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
14 r19.23v ⊢ ∀ k ∈ 1 … N a = A F B → a ∈ ℝ ↔ ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
15 14 albii ⊢ ∀ a ∀ k ∈ 1 … N a = A F B → a ∈ ℝ ↔ ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
16 ralcom4 ⊢ ∀ k ∈ 1 … N ∀ a a = A F B → a ∈ ℝ ↔ ∀ a ∀ k ∈ 1 … N a = A F B → a ∈ ℝ
17 rsp ⊢ ∀ k ∈ 1 … N ∀ a a = A F B → a ∈ ℝ → k ∈ 1 … N → ∀ a a = A F B → a ∈ ℝ
18 2 clel2 ⊢ A F B ∈ ℝ ↔ ∀ a a = A F B → a ∈ ℝ
19 17 18 imbitrrdi ⊢ ∀ k ∈ 1 … N ∀ a a = A F B → a ∈ ℝ → k ∈ 1 … N → A F B ∈ ℝ
20 16 19 sylbir ⊢ ∀ a ∀ k ∈ 1 … N a = A F B → a ∈ ℝ → k ∈ 1 … N → A F B ∈ ℝ
21 15 20 sylbir ⊢ ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ → k ∈ 1 … N → A F B ∈ ℝ
22 13 21 ralrimi ⊢ ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ → ∀ k ∈ 1 … N A F B ∈ ℝ
23 nfra1 ⊢ Ⅎ k ∀ k ∈ 1 … N A F B ∈ ℝ
24 rsp ⊢ ∀ k ∈ 1 … N A F B ∈ ℝ → k ∈ 1 … N → A F B ∈ ℝ
25 eleq1a ⊢ A F B ∈ ℝ → a = A F B → a ∈ ℝ
26 24 25 syl6 ⊢ ∀ k ∈ 1 … N A F B ∈ ℝ → k ∈ 1 … N → a = A F B → a ∈ ℝ
27 23 11 26 rexlimd ⊢ ∀ k ∈ 1 … N A F B ∈ ℝ → ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
28 27 alrimiv ⊢ ∀ k ∈ 1 … N A F B ∈ ℝ → ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ
29 22 28 impbii ⊢ ∀ a ∃ k ∈ 1 … N a = A F B → a ∈ ℝ ↔ ∀ k ∈ 1 … N A F B ∈ ℝ
30 9 29 bitri ⊢ a | ∃ k ∈ 1 … N a = A F B ⊆ ℝ ↔ ∀ k ∈ 1 … N A F B ∈ ℝ
31 8 30 bitri ⊢ ran ⁡ k ∈ 1 … N ⟼ A F B ⊆ ℝ ↔ ∀ k ∈ 1 … N A F B ∈ ℝ
32 6 31 bitri ⊢ k ∈ 1 … N ⟼ A F B : 1 … N ⟶ ℝ ↔ ∀ k ∈ 1 … N A F B ∈ ℝ
33 1 32 bitrdi ⊢ N ∈ ℕ → k ∈ 1 … N ⟼ A F B ∈ 𝔼 ⁡ N ↔ ∀ k ∈ 1 … N A F B ∈ ℝ