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⟼AFB∈𝔼⁡N↔∀k∈1…NAFB∈ℝ

Proof

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