| Step | Hyp | Ref
| Expression |
| 1 | | metidss 33890 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (𝑋 × 𝑋)) |
| 2 | | xpss 5701 |
. . . 4
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
| 3 | 1, 2 | sstrdi 3996 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (V × V)) |
| 4 | | df-rel 5692 |
. . 3
⊢ (Rel
(~Met‘𝐷)
↔ (~Met‘𝐷) ⊆ (V × V)) |
| 5 | 3, 4 | sylibr 234 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → Rel
(~Met‘𝐷)) |
| 6 | 1 | ssbrd 5186 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥(~Met‘𝐷)𝑦 → 𝑥(𝑋 × 𝑋)𝑦)) |
| 7 | 6 | imp 406 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑦) → 𝑥(𝑋 × 𝑋)𝑦) |
| 8 | | brxp 5734 |
. . . 4
⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
| 9 | 7, 8 | sylib 218 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
| 10 | | psmetsym 24320 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
| 11 | 10 | 3expb 1121 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
| 12 | 11 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ (𝑦𝐷𝑥) = 0)) |
| 13 | | metidv 33891 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(~Met‘𝐷)𝑦 ↔ (𝑥𝐷𝑦) = 0)) |
| 14 | | metidv 33891 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑦(~Met‘𝐷)𝑥 ↔ (𝑦𝐷𝑥) = 0)) |
| 15 | 14 | ancom2s 650 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦(~Met‘𝐷)𝑥 ↔ (𝑦𝐷𝑥) = 0)) |
| 16 | 12, 13, 15 | 3bitr4d 311 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(~Met‘𝐷)𝑦 ↔ 𝑦(~Met‘𝐷)𝑥)) |
| 17 | 16 | biimpd 229 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(~Met‘𝐷)𝑦 → 𝑦(~Met‘𝐷)𝑥)) |
| 18 | 17 | impancom 451 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑦) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑦(~Met‘𝐷)𝑥)) |
| 19 | 9, 18 | mpd 15 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑦) → 𝑦(~Met‘𝐷)𝑥) |
| 20 | | simpl 482 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝐷 ∈ (PsMet‘𝑋)) |
| 21 | | simprr 773 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝑦(~Met‘𝐷)𝑧) |
| 22 | 1 | ssbrd 5186 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑦(~Met‘𝐷)𝑧 → 𝑦(𝑋 × 𝑋)𝑧)) |
| 23 | 22 | imp 406 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑦(~Met‘𝐷)𝑧) → 𝑦(𝑋 × 𝑋)𝑧) |
| 24 | | brxp 5734 |
. . . . . . . . 9
⊢ (𝑦(𝑋 × 𝑋)𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) |
| 25 | 23, 24 | sylib 218 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑦(~Met‘𝐷)𝑧) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) |
| 26 | 21, 25 | syldan 591 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) |
| 27 | 26 | simpld 494 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝑦 ∈ 𝑋) |
| 28 | | simprl 771 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝑥(~Met‘𝐷)𝑦) |
| 29 | 28, 9 | syldan 591 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
| 30 | 29 | simpld 494 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝑥 ∈ 𝑋) |
| 31 | 26 | simprd 495 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝑧 ∈ 𝑋) |
| 32 | | psmettri2 24319 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑧) ≤ ((𝑦𝐷𝑥) +𝑒 (𝑦𝐷𝑧))) |
| 33 | 20, 27, 30, 31, 32 | syl13anc 1374 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥𝐷𝑧) ≤ ((𝑦𝐷𝑥) +𝑒 (𝑦𝐷𝑧))) |
| 34 | 29, 11 | syldan 591 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
| 35 | 29, 13 | syldan 591 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥(~Met‘𝐷)𝑦 ↔ (𝑥𝐷𝑦) = 0)) |
| 36 | 28, 35 | mpbid 232 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥𝐷𝑦) = 0) |
| 37 | 34, 36 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑦𝐷𝑥) = 0) |
| 38 | | metidv 33891 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦(~Met‘𝐷)𝑧 ↔ (𝑦𝐷𝑧) = 0)) |
| 39 | 26, 38 | syldan 591 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑦(~Met‘𝐷)𝑧 ↔ (𝑦𝐷𝑧) = 0)) |
| 40 | 21, 39 | mpbid 232 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑦𝐷𝑧) = 0) |
| 41 | 37, 40 | oveq12d 7449 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → ((𝑦𝐷𝑥) +𝑒 (𝑦𝐷𝑧)) = (0 +𝑒
0)) |
| 42 | | 0xr 11308 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
| 43 | | xaddrid 13283 |
. . . . . . 7
⊢ (0 ∈
ℝ* → (0 +𝑒 0) = 0) |
| 44 | 42, 43 | ax-mp 5 |
. . . . . 6
⊢ (0
+𝑒 0) = 0 |
| 45 | 41, 44 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → ((𝑦𝐷𝑥) +𝑒 (𝑦𝐷𝑧)) = 0) |
| 46 | 33, 45 | breqtrd 5169 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥𝐷𝑧) ≤ 0) |
| 47 | | psmetge0 24322 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝑥𝐷𝑧)) |
| 48 | 20, 30, 31, 47 | syl3anc 1373 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 0 ≤ (𝑥𝐷𝑧)) |
| 49 | | psmetcl 24317 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑧) ∈
ℝ*) |
| 50 | 20, 30, 31, 49 | syl3anc 1373 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥𝐷𝑧) ∈
ℝ*) |
| 51 | | xrletri3 13196 |
. . . . 5
⊢ (((𝑥𝐷𝑧) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((𝑥𝐷𝑧) = 0 ↔ ((𝑥𝐷𝑧) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑧)))) |
| 52 | 50, 42, 51 | sylancl 586 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → ((𝑥𝐷𝑧) = 0 ↔ ((𝑥𝐷𝑧) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑧)))) |
| 53 | 46, 48, 52 | mpbir2and 713 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥𝐷𝑧) = 0) |
| 54 | | metidv 33891 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥(~Met‘𝐷)𝑧 ↔ (𝑥𝐷𝑧) = 0)) |
| 55 | 20, 30, 31, 54 | syl12anc 837 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → (𝑥(~Met‘𝐷)𝑧 ↔ (𝑥𝐷𝑧) = 0)) |
| 56 | 53, 55 | mpbird 257 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥(~Met‘𝐷)𝑦 ∧ 𝑦(~Met‘𝐷)𝑧)) → 𝑥(~Met‘𝐷)𝑧) |
| 57 | | psmet0 24318 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐷𝑥) = 0) |
| 58 | | metidv 33891 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥(~Met‘𝐷)𝑥 ↔ (𝑥𝐷𝑥) = 0)) |
| 59 | 58 | anabsan2 674 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥(~Met‘𝐷)𝑥 ↔ (𝑥𝐷𝑥) = 0)) |
| 60 | 57, 59 | mpbird 257 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) → 𝑥(~Met‘𝐷)𝑥) |
| 61 | 1 | ssbrd 5186 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥(~Met‘𝐷)𝑥 → 𝑥(𝑋 × 𝑋)𝑥)) |
| 62 | 61 | imp 406 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑥) → 𝑥(𝑋 × 𝑋)𝑥) |
| 63 | | brxp 5734 |
. . . . 5
⊢ (𝑥(𝑋 × 𝑋)𝑥 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) |
| 64 | 62, 63 | sylib 218 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑥) → (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) |
| 65 | 64 | simpld 494 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥(~Met‘𝐷)𝑥) → 𝑥 ∈ 𝑋) |
| 66 | 60, 65 | impbida 801 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝑥 ∈ 𝑋 ↔ 𝑥(~Met‘𝐷)𝑥)) |
| 67 | 5, 19, 56, 66 | iserd 8771 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
Er 𝑋) |