Step | Hyp | Ref
| Expression |
1 | | f1oi 6086 |
. . 3
⊢ ( I
↾ ℋ): ℋ–1-1-onto→ ℋ |
2 | | f1of 6050 |
. . 3
⊢ (( I
↾ ℋ): ℋ–1-1-onto→ ℋ → ( I ↾ ℋ):
ℋ⟶ ℋ) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ ( I
↾ ℋ): ℋ⟶ ℋ |
4 | | id 22 |
. . . 4
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ+) |
5 | | fvresi 6344 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℋ → (( I
↾ ℋ)‘𝑤) =
𝑤) |
6 | | fvresi 6344 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ → (( I
↾ ℋ)‘𝑥) =
𝑥) |
7 | 5, 6 | oveqan12rd 6569 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥)) = (𝑤 −ℎ 𝑥)) |
8 | 7 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) →
(normℎ‘((( I ↾ ℋ)‘𝑤) −ℎ (( I ↾
ℋ)‘𝑥))) =
(normℎ‘(𝑤 −ℎ 𝑥))) |
9 | 8 | breq1d 4593 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) →
((normℎ‘((( I ↾ ℋ)‘𝑤) −ℎ (( I ↾
ℋ)‘𝑥))) <
𝑦 ↔
(normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦)) |
10 | 9 | biimprd 237 |
. . . . 5
⊢ ((𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ) →
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦)) |
11 | 10 | ralrimiva 2949 |
. . . 4
⊢ (𝑥 ∈ ℋ →
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦)) |
12 | | breq2 4587 |
. . . . . . 7
⊢ (𝑧 = 𝑦 →
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < 𝑦)) |
13 | 12 | imbi1d 330 |
. . . . . 6
⊢ (𝑧 = 𝑦 →
(((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦) ↔
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦))) |
14 | 13 | ralbidv 2969 |
. . . . 5
⊢ (𝑧 = 𝑦 → (∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦) ↔ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦))) |
15 | 14 | rspcev 3282 |
. . . 4
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑤 ∈
ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦)) |
16 | 4, 11, 15 | syl2anr 494 |
. . 3
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+)
→ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦)) |
17 | 16 | rgen2 2958 |
. 2
⊢
∀𝑥 ∈
ℋ ∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦) |
18 | | elcnop 28100 |
. 2
⊢ (( I
↾ ℋ) ∈ ConOp ↔ (( I ↾ ℋ): ℋ⟶
ℋ ∧ ∀𝑥
∈ ℋ ∀𝑦
∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((( I
↾ ℋ)‘𝑤)
−ℎ (( I ↾ ℋ)‘𝑥))) < 𝑦))) |
19 | 3, 17, 18 | mpbir2an 957 |
1
⊢ ( I
↾ ℋ) ∈ ConOp |