| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rpxr 13044 | . . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) | 
| 2 | 1 | ad2antll 729 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) | 
| 3 |  | simpl2 1193 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑅 ∈
ℝ*) | 
| 4 | 2, 3 | ifcld 4572 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈
ℝ*) | 
| 5 |  | rpre 13043 | . . . . . . 7
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) | 
| 6 | 5 | ad2antll 729 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) | 
| 7 |  | rpgt0 13047 | . . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) | 
| 8 | 7 | ad2antll 729 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑟) | 
| 9 |  | simpl3 1194 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑅) | 
| 10 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑟 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → (0 < 𝑟 ↔ 0 < if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 11 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑅 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → (0 < 𝑅 ↔ 0 < if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 12 | 10, 11 | ifboth 4565 | . . . . . . . 8
⊢ ((0 <
𝑟 ∧ 0 < 𝑅) → 0 < if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) | 
| 13 | 8, 9, 12 | syl2anc 584 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 <
if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) | 
| 14 |  | 0xr 11308 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 15 |  | xrltle 13191 | . . . . . . . 8
⊢ ((0
∈ ℝ* ∧ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ*) → (0 <
if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → 0 ≤ if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 16 | 14, 4, 15 | sylancr 587 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (0 <
if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → 0 ≤ if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 17 | 13, 16 | mpd 15 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 0 ≤
if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) | 
| 18 |  | xrmin1 13219 | . . . . . . 7
⊢ ((𝑟 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑟) | 
| 19 | 2, 3, 18 | syl2anc 584 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑟) | 
| 20 |  | xrrege0 13216 | . . . . . 6
⊢
(((if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ* ∧ 𝑟 ∈ ℝ) ∧ (0 ≤
if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∧ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑟)) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ) | 
| 21 | 4, 6, 17, 19, 20 | syl22anc 839 | . . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ) | 
| 22 | 21, 13 | elrpd 13074 | . . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈
ℝ+) | 
| 23 |  | simprl 771 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑧 ∈ 𝑋) | 
| 24 |  | xrmin2 13220 | . . . . . . . 8
⊢ ((𝑟 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑅) | 
| 25 | 2, 3, 24 | syl2anc 584 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑅) | 
| 26 | 23, 4, 25 | 3jca 1129 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑧 ∈ 𝑋 ∧ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ* ∧ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑅)) | 
| 27 |  | stdbdmet.1 | . . . . . . 7
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) | 
| 28 | 27 | stdbdbl 24530 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ* ∧ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑅)) → (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) = (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 29 | 26, 28 | syldan 591 | . . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) = (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 30 | 29 | eqcomd 2743 | . . . 4
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) = (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 31 |  | breq1 5146 | . . . . . 6
⊢ (𝑠 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → (𝑠 ≤ 𝑟 ↔ if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑟)) | 
| 32 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑠 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 33 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑠 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → (𝑧(ball‘𝐷)𝑠) = (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅))) | 
| 34 | 32, 33 | eqeq12d 2753 | . . . . . 6
⊢ (𝑠 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → ((𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠) ↔ (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) = (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)))) | 
| 35 | 31, 34 | anbi12d 632 | . . . . 5
⊢ (𝑠 = if(𝑟 ≤ 𝑅, 𝑟, 𝑅) → ((𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) ↔ (if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑟 ∧ (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) = (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅))))) | 
| 36 | 35 | rspcev 3622 | . . . 4
⊢
((if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ∈ ℝ+ ∧ (if(𝑟 ≤ 𝑅, 𝑟, 𝑅) ≤ 𝑟 ∧ (𝑧(ball‘𝐶)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)) = (𝑧(ball‘𝐷)if(𝑟 ≤ 𝑅, 𝑟, 𝑅)))) → ∃𝑠 ∈ ℝ+ (𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠))) | 
| 37 | 22, 19, 30, 36 | syl12anc 837 | . . 3
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
∃𝑠 ∈
ℝ+ (𝑠 ≤
𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠))) | 
| 38 | 37 | ralrimivva 3202 | . 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → ∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠))) | 
| 39 |  | simp1 1137 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐶 ∈ (∞Met‘𝑋)) | 
| 40 | 27 | stdbdxmet 24528 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 41 |  | stdbdmopn.2 | . . . 4
⊢ 𝐽 = (MetOpen‘𝐶) | 
| 42 |  | eqid 2737 | . . . 4
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) | 
| 43 | 41, 42 | metequiv2 24523 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) → 𝐽 = (MetOpen‘𝐷))) | 
| 44 | 39, 40, 43 | syl2anc 584 | . 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → (∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) → 𝐽 = (MetOpen‘𝐷))) | 
| 45 | 38, 44 | mpd 15 | 1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐽 = (MetOpen‘𝐷)) |