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 ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 elee ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
2 ovex ⊢ ( 𝐴 𝐹 𝐵 ) ∈ V
3 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) )
4 2 3 fnmpti ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) Fn ( 1 ... 𝑁 )
5 df-f ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ↔ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) Fn ( 1 ... 𝑁 ) ∧ ran ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ⊆ ℝ ) )
6 4 5 mpbiran ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ↔ ran ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ⊆ ℝ )
7 3 rnmpt ⊢ ran ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) = { 𝑎 ∣ ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) }
8 7 sseq1i ⊢ ( ran ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ⊆ ℝ ↔ { 𝑎 ∣ ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) } ⊆ ℝ )
9 abss ⊢ ( { 𝑎 ∣ ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) } ⊆ ℝ ↔ ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
10 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 )
11 nfv ⊢ Ⅎ 𝑘 𝑎 ∈ ℝ
12 10 11 nfim ⊢ Ⅎ 𝑘 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ )
13 12 nfal ⊢ Ⅎ 𝑘 ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ )
14 r19.23v ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) ↔ ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
15 14 albii ⊢ ( ∀ 𝑎 ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) ↔ ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
16 ralcom4 ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ∀ 𝑎 ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) ↔ ∀ 𝑎 ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
17 rsp ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ∀ 𝑎 ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) → ∀ 𝑎 ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) ) )
18 2 clel2 ⊢ ( ( 𝐴 𝐹 𝐵 ) ∈ ℝ ↔ ∀ 𝑎 ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
19 17 18 syl6ibr ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ∀ 𝑎 ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )
20 16 19 sylbir ⊢ ( ∀ 𝑎 ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )
21 15 20 sylbir ⊢ ( ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )
22 13 21 ralrimi ⊢ ( ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ )
23 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ
24 rsp ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ → ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )
25 eleq1a ⊢ ( ( 𝐴 𝐹 𝐵 ) ∈ ℝ → ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
26 24 25 syl6 ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ → ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) ) )
27 23 11 26 rexlimd ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ → ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
28 27 alrimiv ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ → ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) )
29 22 28 impbii ⊢ ( ∀ 𝑎 ( ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) → 𝑎 ∈ ℝ ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ )
30 9 29 bitri ⊢ ( { 𝑎 ∣ ∃ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑎 = ( 𝐴 𝐹 𝐵 ) } ⊆ ℝ ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ )
31 8 30 bitri ⊢ ( ran ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ⊆ ℝ ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ )
32 6 31 bitri ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ )
33 1 32 bitrdi ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 𝐹 𝐵 ) ∈ ℝ ) )