| Step | Hyp | Ref
| Expression |
| 1 | | rpxr 9736 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
| 2 | 1 | ad2antll 491 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
| 3 | | simpl2 1003 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑅 ∈
ℝ*) |
| 4 | | xrmincl 11431 |
. . . . . . 7
⊢ ((𝑟 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ*) |
| 5 | 2, 3, 4 | syl2anc 411 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ*) |
| 6 | | rpre 9735 |
. . . . . . 7
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
| 7 | 6 | ad2antll 491 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) |
| 8 | | 0xr 8073 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 9 | 8 | a1i 9 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 ∈
ℝ*) |
| 10 | | rpgt0 9740 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
| 11 | 10 | ad2antll 491 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑟) |
| 12 | | simpl3 1004 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑅) |
| 13 | | xrltmininf 11435 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
→ (0 < inf({𝑟,
𝑅}, ℝ*,
< ) ↔ (0 < 𝑟
∧ 0 < 𝑅))) |
| 14 | 8, 2, 3, 13 | mp3an2i 1353 |
. . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (0 <
inf({𝑟, 𝑅}, ℝ*, < ) ↔ (0
< 𝑟 ∧ 0 < 𝑅))) |
| 15 | 11, 12, 14 | mpbir2and 946 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 <
inf({𝑟, 𝑅}, ℝ*, <
)) |
| 16 | 9, 5, 15 | xrltled 9874 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 ≤
inf({𝑟, 𝑅}, ℝ*, <
)) |
| 17 | | xrmin1inf 11432 |
. . . . . . 7
⊢ ((𝑟 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑟) |
| 18 | 2, 3, 17 | syl2anc 411 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑟) |
| 19 | | xrrege0 9900 |
. . . . . 6
⊢
(((inf({𝑟, 𝑅}, ℝ*, < )
∈ ℝ* ∧ 𝑟 ∈ ℝ) ∧ (0 ≤ inf({𝑟, 𝑅}, ℝ*, < ) ∧
inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑟)) → inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ) |
| 20 | 5, 7, 16, 18, 19 | syl22anc 1250 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ) |
| 21 | 20, 15 | elrpd 9768 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ+) |
| 22 | | simprl 529 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑧 ∈ 𝑋) |
| 23 | | xrmin2inf 11433 |
. . . . . . . 8
⊢ ((𝑟 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑅) |
| 24 | 2, 3, 23 | syl2anc 411 |
. . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑅) |
| 25 | 22, 5, 24 | 3jca 1179 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑧 ∈ 𝑋 ∧ inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ* ∧ inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑅)) |
| 26 | | stdbdmet.1 |
. . . . . . 7
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) |
| 27 | 26 | bdbl 14739 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ inf({𝑟, 𝑅}, ℝ*, < ) ∈
ℝ* ∧ inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑅)) → (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, < )) = (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, <
))) |
| 28 | 25, 27 | syldan 282 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, < )) = (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, <
))) |
| 29 | 28 | eqcomd 2202 |
. . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, <
))) |
| 30 | | breq1 4036 |
. . . . . 6
⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ*, < ) → (𝑠 ≤ 𝑟 ↔ inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑟)) |
| 31 | | oveq2 5930 |
. . . . . . 7
⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ*, < ) → (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, <
))) |
| 32 | | oveq2 5930 |
. . . . . . 7
⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ*, < ) → (𝑧(ball‘𝐷)𝑠) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, <
))) |
| 33 | 31, 32 | eqeq12d 2211 |
. . . . . 6
⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ*, < ) →
((𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠) ↔ (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, <
)))) |
| 34 | 30, 33 | anbi12d 473 |
. . . . 5
⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ*, < ) →
((𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) ↔ (inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑟 ∧ (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, <
))))) |
| 35 | 34 | rspcev 2868 |
. . . 4
⊢
((inf({𝑟, 𝑅}, ℝ*, < )
∈ ℝ+ ∧ (inf({𝑟, 𝑅}, ℝ*, < ) ≤ 𝑟 ∧ (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ*, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ*, < )))) →
∃𝑠 ∈
ℝ+ (𝑠 ≤
𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠))) |
| 36 | 21, 18, 29, 35 | syl12anc 1247 |
. . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
∃𝑠 ∈
ℝ+ (𝑠 ≤
𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠))) |
| 37 | 36 | ralrimivva 2579 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠))) |
| 38 | | simp1 999 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 ∈ (∞Met‘𝑋)) |
| 39 | 26 | bdxmet 14737 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) |
| 40 | | stdbdmopn.2 |
. . . 4
⊢ 𝐽 = (MetOpen‘𝐶) |
| 41 | | eqid 2196 |
. . . 4
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
| 42 | 40, 41 | metequiv2 14732 |
. . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) → 𝐽 = (MetOpen‘𝐷))) |
| 43 | 38, 39, 42 | syl2anc 411 |
. 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) → 𝐽 = (MetOpen‘𝐷))) |
| 44 | 37, 43 | mpd 13 |
1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐽 = (MetOpen‘𝐷)) |