Step | Hyp | Ref
| Expression |
1 | | simp1 1172 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → 𝐷 ∈ (PsMet‘𝑋)) |
2 | | simp3 1174 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → 𝑃 ∈ 𝑋) |
3 | | simpr 479 |
. . . . 5
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) ∧ 𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟)))) ∧ 𝑤 ⊆ 𝑉) → 𝑤 ⊆ 𝑉) |
4 | | vex 3417 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
5 | | eqid 2825 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑟))) = (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟))) |
6 | 5 | elrnmpt 5605 |
. . . . . . . 8
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟))) ↔ ∃𝑟 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑟)))) |
7 | 4, 6 | ax-mp 5 |
. . . . . . 7
⊢ (𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟))) ↔ ∃𝑟 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑟))) |
8 | 7 | biimpi 208 |
. . . . . 6
⊢ (𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟))) → ∃𝑟 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑟))) |
9 | 8 | ad2antlr 720 |
. . . . 5
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) ∧ 𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟)))) ∧ 𝑤 ⊆ 𝑉) → ∃𝑟 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑟))) |
10 | | sseq1 3851 |
. . . . . . 7
⊢ (𝑤 = (◡𝐷 “ (0[,)𝑟)) → (𝑤 ⊆ 𝑉 ↔ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉)) |
11 | 10 | biimpcd 241 |
. . . . . 6
⊢ (𝑤 ⊆ 𝑉 → (𝑤 = (◡𝐷 “ (0[,)𝑟)) → (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉)) |
12 | 11 | reximdv 3224 |
. . . . 5
⊢ (𝑤 ⊆ 𝑉 → (∃𝑟 ∈ ℝ+ 𝑤 = (◡𝐷 “ (0[,)𝑟)) → ∃𝑟 ∈ ℝ+ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉)) |
13 | 3, 9, 12 | sylc 65 |
. . . 4
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) ∧ 𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟)))) ∧ 𝑤 ⊆ 𝑉) → ∃𝑟 ∈ ℝ+ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉) |
14 | 2 | ne0d 4151 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → 𝑋 ≠ ∅) |
15 | | simp2 1173 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → 𝑉 ∈ (metUnif‘𝐷)) |
16 | | metuel 22739 |
. . . . . 6
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ (metUnif‘𝐷) ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟)))𝑤 ⊆ 𝑉))) |
17 | 16 | simplbda 495 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑉 ∈ (metUnif‘𝐷)) → ∃𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟)))𝑤 ⊆ 𝑉) |
18 | 14, 1, 15, 17 | syl21anc 873 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑤 ∈ ran (𝑟 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑟)))𝑤 ⊆ 𝑉) |
19 | 13, 18 | r19.29a 3288 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑟 ∈ ℝ+ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉) |
20 | | imass1 5741 |
. . . . . 6
⊢ ((◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉 → ((◡𝐷 “ (0[,)𝑟)) “ {𝑃}) ⊆ (𝑉 “ {𝑃})) |
21 | 20 | reximi 3219 |
. . . . 5
⊢
(∃𝑟 ∈
ℝ+ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉 → ∃𝑟 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑟)) “ {𝑃}) ⊆ (𝑉 “ {𝑃})) |
22 | | blval2 22737 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑟) = ((◡𝐷 “ (0[,)𝑟)) “ {𝑃})) |
23 | 22 | sseq1d 3857 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → ((𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃}) ↔ ((◡𝐷 “ (0[,)𝑟)) “ {𝑃}) ⊆ (𝑉 “ {𝑃}))) |
24 | 23 | 3expa 1153 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → ((𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃}) ↔ ((◡𝐷 “ (0[,)𝑟)) “ {𝑃}) ⊆ (𝑉 “ {𝑃}))) |
25 | 24 | rexbidva 3259 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃}) ↔ ∃𝑟 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑟)) “ {𝑃}) ⊆ (𝑉 “ {𝑃}))) |
26 | 21, 25 | syl5ibr 238 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉 → ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃}))) |
27 | 26 | imp 397 |
. . 3
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ ∃𝑟 ∈ ℝ+ (◡𝐷 “ (0[,)𝑟)) ⊆ 𝑉) → ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃})) |
28 | 1, 2, 19, 27 | syl21anc 873 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃})) |
29 | | blssexps 22601 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑎 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ (𝑉 “ {𝑃})) ↔ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃}))) |
30 | 29 | 3adant2 1167 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → (∃𝑎 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ (𝑉 “ {𝑃})) ↔ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ (𝑉 “ {𝑃}))) |
31 | 28, 30 | mpbird 249 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑎 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ (𝑉 “ {𝑃}))) |