| Step | Hyp | Ref
| Expression |
| 1 | | df-hlim 30991 |
. . 3
⊢
⇝𝑣 = {〈𝑓, 𝑥〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)} |
| 2 | 1 | relopabiv 5830 |
. 2
⊢ Rel
⇝𝑣 |
| 3 | | relres 6023 |
. 2
⊢ Rel
((⇝𝑡‘𝐽) ↾ ( ℋ ↑m
ℕ)) |
| 4 | 1 | eleq2i 2833 |
. . 3
⊢
(〈𝑓, 𝑥〉 ∈
⇝𝑣 ↔ 〈𝑓, 𝑥〉 ∈ {〈𝑓, 𝑥〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)}) |
| 5 | | opabidw 5529 |
. . 3
⊢
(〈𝑓, 𝑥〉 ∈ {〈𝑓, 𝑥〉 ∣ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)} ↔ ((𝑓:ℕ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 6 | | h2hl.3 |
. . . . . . . 8
⊢ ℋ
= (BaseSet‘𝑈) |
| 7 | 6 | hlex 30917 |
. . . . . . 7
⊢ ℋ
∈ V |
| 8 | | nnex 12272 |
. . . . . . 7
⊢ ℕ
∈ V |
| 9 | 7, 8 | elmap 8911 |
. . . . . 6
⊢ (𝑓 ∈ ( ℋ
↑m ℕ) ↔ 𝑓:ℕ⟶ ℋ) |
| 10 | 9 | anbi1i 624 |
. . . . 5
⊢ ((𝑓 ∈ ( ℋ
↑m ℕ) ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)) ↔ (𝑓:ℕ⟶ ℋ ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽))) |
| 11 | | df-br 5144 |
. . . . . . 7
⊢ (𝑓(⇝𝑡‘𝐽)𝑥 ↔ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)) |
| 12 | | h2hl.5 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘𝐷) |
| 13 | | h2hl.2 |
. . . . . . . . . 10
⊢ 𝑈 ∈ NrmCVec |
| 14 | | h2hl.4 |
. . . . . . . . . . 11
⊢ 𝐷 = (IndMet‘𝑈) |
| 15 | 6, 14 | imsxmet 30711 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘
ℋ)) |
| 16 | 13, 15 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶ ℋ →
𝐷 ∈ (∞Met‘
ℋ)) |
| 17 | | nnuz 12921 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
| 18 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶ ℋ →
1 ∈ ℤ) |
| 19 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) →
(𝑓‘𝑘) = (𝑓‘𝑘)) |
| 20 | | id 22 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶ ℋ →
𝑓:ℕ⟶
ℋ) |
| 21 | 12, 16, 17, 18, 19, 20 | lmmbrf 25296 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶ ℋ →
(𝑓(⇝𝑡‘𝐽)𝑥 ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦))) |
| 22 | | eluznn 12960 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
| 23 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) →
(𝑓‘𝑘) ∈ ℋ) |
| 24 | | h2hl.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑈 = 〈〈
+ℎ , ·ℎ 〉,
normℎ〉 |
| 25 | 24, 13, 6, 14 | h2hmetdval 30997 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓‘𝑘) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑓‘𝑘)𝐷𝑥) = (normℎ‘((𝑓‘𝑘) −ℎ 𝑥))) |
| 26 | 23, 25 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) ∧
𝑥 ∈ ℋ) →
((𝑓‘𝑘)𝐷𝑥) = (normℎ‘((𝑓‘𝑘) −ℎ 𝑥))) |
| 27 | 26 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑘 ∈ ℕ) ∧
𝑥 ∈ ℋ) →
(((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 28 | 27 | an32s 652 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑘 ∈ ℕ) →
(((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 29 | 22, 28 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
(𝑗 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘𝑗))) → (((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 30 | 29 | anassrs 467 |
. . . . . . . . . . . 12
⊢ ((((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑗 ∈ ℕ) ∧
𝑘 ∈
(ℤ≥‘𝑗)) → (((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔
(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 31 | 30 | ralbidva 3176 |
. . . . . . . . . . 11
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 32 | 31 | rexbidva 3177 |
. . . . . . . . . 10
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 33 | 32 | ralbidv 3178 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦 ↔ ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) |
| 34 | 33 | pm5.32da 579 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶ ℋ →
((𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘)𝐷𝑥) < 𝑦) ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
| 35 | 21, 34 | bitrd 279 |
. . . . . . 7
⊢ (𝑓:ℕ⟶ ℋ →
(𝑓(⇝𝑡‘𝐽)𝑥 ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
| 36 | 11, 35 | bitr3id 285 |
. . . . . 6
⊢ (𝑓:ℕ⟶ ℋ →
(〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽) ↔ (𝑥 ∈ ℋ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
| 37 | 36 | pm5.32i 574 |
. . . . 5
⊢ ((𝑓:ℕ⟶ ℋ ∧
〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)) ↔ (𝑓:ℕ⟶ ℋ ∧ (𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
| 38 | 10, 37 | bitr2i 276 |
. . . 4
⊢ ((𝑓:ℕ⟶ ℋ ∧
(𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦)) ↔ (𝑓 ∈ ( ℋ ↑m ℕ)
∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽))) |
| 39 | | anass 468 |
. . . 4
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦) ↔ (𝑓:ℕ⟶ ℋ ∧ (𝑥 ∈ ℋ ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦))) |
| 40 | | opelres 6003 |
. . . . 5
⊢ (𝑥 ∈ V → (〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ ↑m
ℕ)) ↔ (𝑓 ∈
( ℋ ↑m ℕ) ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽)))) |
| 41 | 40 | elv 3485 |
. . . 4
⊢
(〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ ↑m
ℕ)) ↔ (𝑓 ∈
( ℋ ↑m ℕ) ∧ 〈𝑓, 𝑥〉 ∈
(⇝𝑡‘𝐽))) |
| 42 | 38, 39, 41 | 3bitr4i 303 |
. . 3
⊢ (((𝑓:ℕ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝑓‘𝑘) −ℎ 𝑥)) < 𝑦) ↔ 〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ ↑m
ℕ))) |
| 43 | 4, 5, 42 | 3bitri 297 |
. 2
⊢
(〈𝑓, 𝑥〉 ∈
⇝𝑣 ↔ 〈𝑓, 𝑥〉 ∈
((⇝𝑡‘𝐽) ↾ ( ℋ ↑m
ℕ))) |
| 44 | 2, 3, 43 | eqrelriiv 5800 |
1
⊢
⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ
↑m ℕ)) |