| Step | Hyp | Ref
| Expression |
| 1 | | xmeter.1 |
. . . . 5
⊢ ∼ =
(◡𝐷 “ ℝ) |
| 2 | | cnvimass 6100 |
. . . . 5
⊢ (◡𝐷 “ ℝ) ⊆ dom 𝐷 |
| 3 | 1, 2 | eqsstri 4030 |
. . . 4
⊢ ∼
⊆ dom 𝐷 |
| 4 | | xmetf 24339 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 5 | 3, 4 | fssdm 6755 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ ⊆ (𝑋 × 𝑋)) |
| 6 | | relxp 5703 |
. . 3
⊢ Rel
(𝑋 × 𝑋) |
| 7 | | relss 5791 |
. . 3
⊢ ( ∼
⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel ∼ )) |
| 8 | 5, 6, 7 | mpisyl 21 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → Rel ∼ ) |
| 9 | 1 | xmeterval 24442 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ))) |
| 10 | 9 | biimpa 476 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ)) |
| 11 | 10 | simp2d 1144 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝑦 ∈ 𝑋) |
| 12 | 10 | simp1d 1143 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝑥 ∈ 𝑋) |
| 13 | | simpl 482 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝐷 ∈ (∞Met‘𝑋)) |
| 14 | | xmetsym 24357 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
| 15 | 13, 12, 11, 14 | syl3anc 1373 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
| 16 | 10 | simp3d 1145 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ) |
| 17 | 15, 16 | eqeltrrd 2842 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑦𝐷𝑥) ∈ ℝ) |
| 18 | 1 | xmeterval 24442 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑦𝐷𝑥) ∈ ℝ))) |
| 19 | 18 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑦𝐷𝑥) ∈ ℝ))) |
| 20 | 11, 12, 17, 19 | mpbir3and 1343 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝑦 ∼ 𝑥) |
| 21 | 12 | adantrr 717 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∈ 𝑋) |
| 22 | 1 | xmeterval 24442 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑦𝐷𝑧) ∈ ℝ))) |
| 23 | 22 | biimpa 476 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∼ 𝑧) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑦𝐷𝑧) ∈ ℝ)) |
| 24 | 23 | adantrl 716 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑦𝐷𝑧) ∈ ℝ)) |
| 25 | 24 | simp2d 1144 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑧 ∈ 𝑋) |
| 26 | | simpl 482 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 27 | 16 | adantrr 717 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥𝐷𝑦) ∈ ℝ) |
| 28 | 24 | simp3d 1145 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦𝐷𝑧) ∈ ℝ) |
| 29 | | rexadd 13274 |
. . . . . 6
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ (𝑦𝐷𝑧) ∈ ℝ) → ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) = ((𝑥𝐷𝑦) + (𝑦𝐷𝑧))) |
| 30 | | readdcl 11238 |
. . . . . 6
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ (𝑦𝐷𝑧) ∈ ℝ) → ((𝑥𝐷𝑦) + (𝑦𝐷𝑧)) ∈ ℝ) |
| 31 | 29, 30 | eqeltrd 2841 |
. . . . 5
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ (𝑦𝐷𝑧) ∈ ℝ) → ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) ∈ ℝ) |
| 32 | 27, 28, 31 | syl2anc 584 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) ∈ ℝ) |
| 33 | 11 | adantrr 717 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑦 ∈ 𝑋) |
| 34 | | xmettri 24361 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑧) ≤ ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧))) |
| 35 | 26, 21, 25, 33, 34 | syl13anc 1374 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥𝐷𝑧) ≤ ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧))) |
| 36 | | xmetlecl 24356 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) ∈ ℝ ∧ (𝑥𝐷𝑧) ≤ ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)))) → (𝑥𝐷𝑧) ∈ ℝ) |
| 37 | 26, 21, 25, 32, 35, 36 | syl122anc 1381 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥𝐷𝑧) ∈ ℝ) |
| 38 | 1 | xmeterval 24442 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥𝐷𝑧) ∈ ℝ))) |
| 39 | 38 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥𝐷𝑧) ∈ ℝ))) |
| 40 | 21, 25, 37, 39 | mpbir3and 1343 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∼ 𝑧) |
| 41 | | xmet0 24352 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐷𝑥) = 0) |
| 42 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 43 | 41, 42 | eqeltrdi 2849 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐷𝑥) ∈ ℝ) |
| 44 | 43 | ex 412 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 → (𝑥𝐷𝑥) ∈ ℝ)) |
| 45 | 44 | pm4.71rd 562 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ ((𝑥𝐷𝑥) ∈ ℝ ∧ 𝑥 ∈ 𝑋))) |
| 46 | | df-3an 1089 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (𝑥𝐷𝑥) ∈ ℝ)) |
| 47 | | anidm 564 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ↔ 𝑥 ∈ 𝑋) |
| 48 | 47 | anbi2ci 625 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (𝑥𝐷𝑥) ∈ ℝ) ↔ ((𝑥𝐷𝑥) ∈ ℝ ∧ 𝑥 ∈ 𝑋)) |
| 49 | 46, 48 | bitri 275 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ) ↔ ((𝑥𝐷𝑥) ∈ ℝ ∧ 𝑥 ∈ 𝑋)) |
| 50 | 45, 49 | bitr4di 289 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ))) |
| 51 | 1 | xmeterval 24442 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ))) |
| 52 | 50, 51 | bitr4d 282 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∼ 𝑥)) |
| 53 | 8, 20, 40, 52 | iserd 8771 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) |