| Step | Hyp | Ref
| Expression |
| 1 | | rpxr 13044 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
| 2 | | blvalps 24395 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) |
| 3 | 1, 2 | syl3an3 1166 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) |
| 4 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥(𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈
ℝ+) |
| 5 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑥((◡𝐷 “ (0[,)𝑅)) “ {𝑃}) |
| 6 | | nfrab1 3457 |
. . 3
⊢
Ⅎ𝑥{𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅} |
| 7 | | psmetf 24316 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 8 | | ffn 6736 |
. . . . . . 7
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → 𝐷 Fn (𝑋 × 𝑋)) |
| 9 | | elpreima 7078 |
. . . . . . 7
⊢ (𝐷 Fn (𝑋 × 𝑋) → (〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)) ↔ (〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)))) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)) ↔ (〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)))) |
| 11 | 10 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) →
(〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)) ↔ (〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)))) |
| 12 | | opelxp 5721 |
. . . . . . . . . 10
⊢
(〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ↔ (𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) |
| 13 | 12 | baib 535 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝑋 → (〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ↔ 𝑥 ∈ 𝑋)) |
| 14 | 13 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) →
(〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ↔ 𝑥 ∈ 𝑋)) |
| 15 | 14 | biimpd 229 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) →
(〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) → 𝑥 ∈ 𝑋)) |
| 16 | 15 | adantrd 491 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) →
((〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)) → 𝑥 ∈ 𝑋)) |
| 17 | | simprl 771 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)) → 𝑥 ∈ 𝑋) |
| 18 | 17 | ex 412 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝑋)) |
| 19 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → 𝑃 ∈ 𝑋) |
| 20 | 19, 13 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ↔ 𝑥 ∈ 𝑋)) |
| 21 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑃𝐷𝑥) = (𝐷‘〈𝑃, 𝑥〉) |
| 22 | 21 | eleq1i 2832 |
. . . . . . . . 9
⊢ ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)) |
| 23 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 24 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈
ℝ+) |
| 25 | 24 | rpxrd 13078 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈
ℝ*) |
| 26 | | elico1 13430 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 𝑅 ∈ ℝ*) → ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ ((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 27 | 23, 25, 26 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ ((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 28 | | df-3an 1089 |
. . . . . . . . . . 11
⊢ (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅) ↔ (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥)) ∧ (𝑃𝐷𝑥) < 𝑅)) |
| 29 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ (PsMet‘𝑋)) |
| 30 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 31 | | psmetcl 24317 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈
ℝ*) |
| 32 | 29, 19, 30, 31 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈
ℝ*) |
| 33 | | psmetge0 24322 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝑃𝐷𝑥)) |
| 34 | 29, 19, 30, 33 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝑃𝐷𝑥)) |
| 35 | 32, 34 | jca 511 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥))) |
| 36 | 35 | biantrurd 532 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷𝑥) < 𝑅 ↔ (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥)) ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 37 | 28, 36 | bitr4id 290 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤
(𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅) ↔ (𝑃𝐷𝑥) < 𝑅)) |
| 38 | 27, 37 | bitrd 279 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ (𝑃𝐷𝑥) < 𝑅)) |
| 39 | 22, 38 | bitr3id 285 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → ((𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅) ↔ (𝑃𝐷𝑥) < 𝑅)) |
| 40 | 20, 39 | anbi12d 632 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → ((〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 41 | 40 | ex 412 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑥 ∈ 𝑋 → ((〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))) |
| 42 | 16, 18, 41 | pm5.21ndd 379 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) →
((〈𝑃, 𝑥〉 ∈ (𝑋 × 𝑋) ∧ (𝐷‘〈𝑃, 𝑥〉) ∈ (0[,)𝑅)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 43 | 11, 42 | bitrd 279 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) →
(〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 44 | | elimasng 6107 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ 〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)))) |
| 45 | 44 | elvd 3486 |
. . . . 5
⊢ (𝑃 ∈ 𝑋 → (𝑥 ∈ ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ 〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)))) |
| 46 | 45 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑥 ∈ ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ 〈𝑃, 𝑥〉 ∈ (◡𝐷 “ (0[,)𝑅)))) |
| 47 | | rabid 3458 |
. . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅} ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)) |
| 48 | 47 | a1i 11 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑥 ∈ {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅} ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
| 49 | 43, 46, 48 | 3bitr4d 311 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑥 ∈ ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ 𝑥 ∈ {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅})) |
| 50 | 4, 5, 6, 49 | eqrd 4003 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) |
| 51 | 3, 50 | eqtr4d 2780 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = ((◡𝐷 “ (0[,)𝑅)) “ {𝑃})) |