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