Step | Hyp | Ref
| Expression |
1 | | df-rab 3074 |
. 2
⊢ {𝑡 ∈ ( ℋ
↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)} = {𝑡 ∣ (𝑡 ∈ ( ℋ ↑m ℋ)
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))} |
2 | | df-cnop 30181 |
. 2
⊢ ContOp =
{𝑡 ∈ ( ℋ
↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)} |
3 | | hhcn.1 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (normℎ
∘ −ℎ ) |
4 | 3 | hilmetdval 29537 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑥𝐷𝑤) = (normℎ‘(𝑥 −ℎ
𝑤))) |
5 | | normsub 29484 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) →
(normℎ‘(𝑥 −ℎ 𝑤)) =
(normℎ‘(𝑤 −ℎ 𝑥))) |
6 | 4, 5 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑥𝐷𝑤) = (normℎ‘(𝑤 −ℎ
𝑥))) |
7 | 6 | adantll 710 |
. . . . . . . . . . 11
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑤 ∈ ℋ) →
(𝑥𝐷𝑤) = (normℎ‘(𝑤 −ℎ
𝑥))) |
8 | 7 | breq1d 5088 |
. . . . . . . . . 10
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑤 ∈ ℋ) →
((𝑥𝐷𝑤) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < 𝑧)) |
9 | | ffvelrn 6953 |
. . . . . . . . . . . . . 14
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑡‘𝑥) ∈ ℋ) |
10 | | ffvelrn 6953 |
. . . . . . . . . . . . . 14
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑤 ∈ ℋ) →
(𝑡‘𝑤) ∈ ℋ) |
11 | 9, 10 | anim12dan 618 |
. . . . . . . . . . . . 13
⊢ ((𝑡: ℋ⟶ ℋ ∧
(𝑥 ∈ ℋ ∧
𝑤 ∈ ℋ)) →
((𝑡‘𝑥) ∈ ℋ ∧ (𝑡‘𝑤) ∈ ℋ)) |
12 | 3 | hilmetdval 29537 |
. . . . . . . . . . . . . 14
⊢ (((𝑡‘𝑥) ∈ ℋ ∧ (𝑡‘𝑤) ∈ ℋ) → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) = (normℎ‘((𝑡‘𝑥) −ℎ (𝑡‘𝑤)))) |
13 | | normsub 29484 |
. . . . . . . . . . . . . 14
⊢ (((𝑡‘𝑥) ∈ ℋ ∧ (𝑡‘𝑤) ∈ ℋ) →
(normℎ‘((𝑡‘𝑥) −ℎ (𝑡‘𝑤))) = (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥)))) |
14 | 12, 13 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ (((𝑡‘𝑥) ∈ ℋ ∧ (𝑡‘𝑤) ∈ ℋ) → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) = (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥)))) |
15 | 11, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑡: ℋ⟶ ℋ ∧
(𝑥 ∈ ℋ ∧
𝑤 ∈ ℋ)) →
((𝑡‘𝑥)𝐷(𝑡‘𝑤)) = (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥)))) |
16 | 15 | anassrs 467 |
. . . . . . . . . . 11
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑤 ∈ ℋ) →
((𝑡‘𝑥)𝐷(𝑡‘𝑤)) = (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥)))) |
17 | 16 | breq1d 5088 |
. . . . . . . . . 10
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑤 ∈ ℋ) →
(((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦 ↔
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)) |
18 | 8, 17 | imbi12d 344 |
. . . . . . . . 9
⊢ (((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) ∧
𝑤 ∈ ℋ) →
(((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦) ↔
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
19 | 18 | ralbidva 3121 |
. . . . . . . 8
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∀𝑤 ∈ ℋ
((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦) ↔ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
20 | 19 | rexbidv 3227 |
. . . . . . 7
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∃𝑧 ∈
ℝ+ ∀𝑤 ∈ ℋ ((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦) ↔ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
21 | 20 | ralbidv 3122 |
. . . . . 6
⊢ ((𝑡: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
22 | 21 | ralbidva 3121 |
. . . . 5
⊢ (𝑡: ℋ⟶ ℋ →
(∀𝑥 ∈ ℋ
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
23 | 22 | pm5.32i 574 |
. . . 4
⊢ ((𝑡: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦)) ↔ (𝑡: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
24 | 3 | hilxmet 29536 |
. . . . 5
⊢ 𝐷 ∈ (∞Met‘
ℋ) |
25 | | hhcn.2 |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
26 | 25, 25 | metcn 23680 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘
ℋ) ∧ 𝐷 ∈
(∞Met‘ ℋ)) → (𝑡 ∈ (𝐽 Cn 𝐽) ↔ (𝑡: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ ℋ ((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦)))) |
27 | 24, 24, 26 | mp2an 688 |
. . . 4
⊢ (𝑡 ∈ (𝐽 Cn 𝐽) ↔ (𝑡: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ ℋ ((𝑥𝐷𝑤) < 𝑧 → ((𝑡‘𝑥)𝐷(𝑡‘𝑤)) < 𝑦))) |
28 | | ax-hilex 29340 |
. . . . . 6
⊢ ℋ
∈ V |
29 | 28, 28 | elmap 8633 |
. . . . 5
⊢ (𝑡 ∈ ( ℋ
↑m ℋ) ↔ 𝑡: ℋ⟶ ℋ) |
30 | 29 | anbi1i 623 |
. . . 4
⊢ ((𝑡 ∈ ( ℋ
↑m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)) ↔ (𝑡: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
31 | 23, 27, 30 | 3bitr4i 302 |
. . 3
⊢ (𝑡 ∈ (𝐽 Cn 𝐽) ↔ (𝑡 ∈ ( ℋ ↑m ℋ)
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))) |
32 | 31 | abbi2i 2880 |
. 2
⊢ (𝐽 Cn 𝐽) = {𝑡 ∣ (𝑡 ∈ ( ℋ ↑m ℋ)
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 →
(normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦))} |
33 | 1, 2, 32 | 3eqtr4i 2777 |
1
⊢ ContOp =
(𝐽 Cn 𝐽) |