Proof of Theorem metequiv2
Step | Hyp | Ref
| Expression |
1 | | simprrr 535 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) |
2 | | simplll 528 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝐶 ∈ (∞Met‘𝑋)) |
3 | | simplr 525 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝑥 ∈ 𝑋) |
4 | | simprlr 533 |
. . . . . . . . . . . . 13
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝑠 ∈ ℝ+) |
5 | 4 | rpxrd 9643 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝑠 ∈ ℝ*) |
6 | | simprll 532 |
. . . . . . . . . . . . 13
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝑟 ∈ ℝ+) |
7 | 6 | rpxrd 9643 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝑟 ∈ ℝ*) |
8 | | simprrl 534 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝑠 ≤ 𝑟) |
9 | | ssbl 13181 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑠 ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
∧ 𝑠 ≤ 𝑟) → (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)) |
10 | 2, 3, 5, 7, 8, 9 | syl221anc 1244 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)) |
11 | 1, 10 | eqsstrrd 3184 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)) |
12 | | simpllr 529 |
. . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → 𝐷 ∈ (∞Met‘𝑋)) |
13 | | ssbl 13181 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑠 ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
∧ 𝑠 ≤ 𝑟) → (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)) |
14 | 12, 3, 5, 7, 8, 13 | syl221anc 1244 |
. . . . . . . . . . 11
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)) |
15 | 1, 14 | eqsstrd 3183 |
. . . . . . . . . 10
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)) |
16 | 11, 15 | jca 304 |
. . . . . . . . 9
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ ((𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+)
∧ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)))) → ((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟))) |
17 | 16 | expr 373 |
. . . . . . . 8
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ ((𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → ((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
18 | 17 | anassrs 398 |
. . . . . . 7
⊢
(((((𝐶 ∈
(∞Met‘𝑋) ∧
𝐷 ∈
(∞Met‘𝑋)) ∧
𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑠 ∈ ℝ+)
→ ((𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → ((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
19 | 18 | reximdva 2572 |
. . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) →
(∃𝑠 ∈
ℝ+ (𝑠 ≤
𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → ∃𝑠 ∈ ℝ+ ((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
20 | | r19.40 2624 |
. . . . . 6
⊢
(∃𝑠 ∈
ℝ+ ((𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)) → (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟))) |
21 | 19, 20 | syl6 33 |
. . . . 5
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) →
(∃𝑠 ∈
ℝ+ (𝑠 ≤
𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
22 | 21 | ralimdva 2537 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → ∀𝑟 ∈ ℝ+ (∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
23 | | r19.26 2596 |
. . . 4
⊢
(∀𝑟 ∈
ℝ+ (∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)) ↔ (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟))) |
24 | 22, 23 | syl6ib 160 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) ∧ 𝑥 ∈ 𝑋) → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
25 | 24 | ralimdva 2537 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → ∀𝑥 ∈ 𝑋 (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
26 | | metequiv.3 |
. . 3
⊢ 𝐽 = (MetOpen‘𝐶) |
27 | | metequiv.4 |
. . 3
⊢ 𝐾 = (MetOpen‘𝐷) |
28 | 26, 27 | metequiv 13250 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 = 𝐾 ↔ ∀𝑥 ∈ 𝑋 (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐶)𝑠) ⊆ (𝑥(ball‘𝐷)𝑟)))) |
29 | 25, 28 | sylibrd 168 |
1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → 𝐽 = 𝐾)) |