Step | Hyp | Ref
| Expression |
1 | | df-hlim 27213 |
. . 3
⊢
⇝𝑣 = {〈𝑓, 𝑥〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)} |
2 | 1 | relopabi 5167 |
. 2
⊢ Rel
⇝𝑣 |
3 | | relres 5346 |
. 2
⊢ Rel
((⇝𝑡‘𝐽) ↾ ( ℋ
↑𝑚 ℕ)) |
4 | 1 | eleq2i 2680 |
. . 3
⊢
(〈𝑓, 𝑥〉 ∈
⇝𝑣 ↔ 〈𝑓, 𝑥〉 ∈ {〈𝑓, 𝑥〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)}) |
5 | | opabid 4907 |
. . 3
⊢
(〈𝑓, 𝑥〉 ∈ {〈𝑓, 𝑥〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)} ↔ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
6 | | ancom 465 |
. . . . 5
⊢
((〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽) ∧ 𝑓 ∈ ( ℋ ↑𝑚
ℕ)) ↔ (𝑓 ∈
( ℋ ↑𝑚 ℕ) ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽))) |
7 | | h2hl.3 |
. . . . . . . 8
⊢ ℋ
= (BaseSet‘𝑈) |
8 | 7 | hlex 27138 |
. . . . . . 7
⊢ ℋ
∈ V |
9 | | nnex 10903 |
. . . . . . 7
⊢ ℕ
∈ V |
10 | 8, 9 | elmap 7772 |
. . . . . 6
⊢ (𝑓 ∈ ( ℋ
↑𝑚 ℕ) ↔ 𝑓:ℕ⟶ ℋ) |
11 | 10 | anbi1i 727 |
. . . . 5
⊢ ((𝑓 ∈ ( ℋ
↑𝑚 ℕ) ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)) ↔ (𝑓:ℕ⟶ ℋ ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽))) |
12 | | df-br 4584 |
. . . . . . 7
⊢ (𝑓(⇝𝑡‘𝐽)𝑥 ↔ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)) |
13 | | h2hl.5 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘𝐷) |
14 | | h2hl.2 |
. . . . . . . . . 10
⊢ 𝑈 ∈ NrmCVec |
15 | | h2hl.4 |
. . . . . . . . . . 11
⊢ 𝐷 = (IndMet‘𝑈) |
16 | 7, 15 | imsxmet 26931 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘
ℋ)) |
17 | 14, 16 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶ ℋ →
𝐷 ∈ (∞Met‘
ℋ)) |
18 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
19 | | 1zzd 11285 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶ ℋ →
1 ∈ ℤ) |
20 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) →
(𝑓‘𝑘) = (𝑓‘𝑘)) |
21 | | id 22 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶ ℋ →
𝑓:ℕ⟶
ℋ) |
22 | 13, 17, 18, 19, 20, 21 | lmmbrf 22868 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶ ℋ →
(𝑓(⇝𝑡‘𝐽)𝑥 ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦))) |
23 | | eluznn 11634 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
24 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) →
(𝑓‘𝑘) ∈ ℋ) |
25 | | h2hl.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑈 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
26 | 25, 14, 7, 15 | h2hmetdval 27219 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓‘𝑘) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑓‘𝑘)𝐷𝑥) = (normℎ‘((𝑓‘𝑘) −ℎ 𝑥))) |
27 | 24, 26 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) ∧
𝑥 ∈ ℋ) →
((𝑓‘𝑘)𝐷𝑥) = (normℎ‘((𝑓‘𝑘) −ℎ 𝑥))) |
28 | 27 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) ∧
𝑥 ∈ ℋ) →
(((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
29 | 28 | an32s 842 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑘 ∈ ℕ) →
(((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
30 | 23, 29 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
31 | 30 | anassrs 678 |
. . . . . . . . . . . 12
⊢ ((((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑗 ∈ ℕ) ∧
𝑘 ∈
(ℤ≥‘𝑗)) → (((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
32 | 31 | ralbidva 2968 |
. . . . . . . . . . 11
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
33 | 32 | rexbidva 3031 |
. . . . . . . . . 10
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
34 | 33 | ralbidv 2969 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔ ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
35 | 34 | pm5.32da 671 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶ ℋ →
((𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦) ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
36 | 22, 35 | bitrd 267 |
. . . . . . 7
⊢ (𝑓:ℕ⟶ ℋ →
(𝑓(⇝𝑡‘𝐽)𝑥 ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
37 | 12, 36 | syl5bbr 273 |
. . . . . 6
⊢ (𝑓:ℕ⟶ ℋ →
(〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽) ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
38 | 37 | pm5.32i 667 |
. . . . 5
⊢ ((𝑓:ℕ⟶ ℋ ∧
〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)) ↔ (𝑓:ℕ⟶ ℋ ∧ (𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
39 | 6, 11, 38 | 3bitrri 286 |
. . . 4
⊢ ((𝑓:ℕ⟶ ℋ ∧
(𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) ↔ (〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽) ∧ 𝑓 ∈ ( ℋ ↑𝑚
ℕ))) |
40 | | anass 679 |
. . . 4
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦) ↔ (𝑓:ℕ⟶ ℋ ∧ (𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
41 | | vex 3176 |
. . . . 5
⊢ 𝑥 ∈ V |
42 | 41 | opelres 5322 |
. . . 4
⊢
(〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ
↑𝑚 ℕ)) ↔ (〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽) ∧ 𝑓 ∈ ( ℋ ↑𝑚
ℕ))) |
43 | 39, 40, 42 | 3bitr4i 291 |
. . 3
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦) ↔ 〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ
↑𝑚 ℕ))) |
44 | 4, 5, 43 | 3bitri 285 |
. 2
⊢
(〈𝑓, 𝑥〉 ∈
⇝𝑣 ↔ 〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ
↑𝑚 ℕ))) |
45 | 2, 3, 44 | eqrelriiv 5137 |
1
⊢
⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ
↑𝑚 ℕ)) |