Step | Hyp | Ref
| Expression |
1 | | xmeter.1 |
. . . . 5
⊢ ∼ =
(◡𝐷 “ ℝ) |
2 | | cnvimass 5404 |
. . . . 5
⊢ (◡𝐷 “ ℝ) ⊆ dom 𝐷 |
3 | 1, 2 | eqsstri 3598 |
. . . 4
⊢ ∼
⊆ dom 𝐷 |
4 | | xmetf 21944 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
5 | | fdm 5964 |
. . . . 5
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → dom
𝐷 = (𝑋 × 𝑋)) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → dom 𝐷 = (𝑋 × 𝑋)) |
7 | 3, 6 | syl5sseq 3616 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ ⊆ (𝑋 × 𝑋)) |
8 | | relxp 5150 |
. . 3
⊢ Rel
(𝑋 × 𝑋) |
9 | | relss 5129 |
. . 3
⊢ ( ∼
⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel ∼ )) |
10 | 7, 8, 9 | mpisyl 21 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → Rel ∼ ) |
11 | 1 | xmeterval 22047 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ))) |
12 | 11 | biimpa 500 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝑥𝐷𝑦) ∈ ℝ)) |
13 | 12 | simp2d 1067 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝑦 ∈ 𝑋) |
14 | 12 | simp1d 1066 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝑥 ∈ 𝑋) |
15 | | simpl 472 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝐷 ∈ (∞Met‘𝑋)) |
16 | | xmetsym 21962 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
17 | 15, 14, 13, 16 | syl3anc 1318 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) |
18 | 12 | simp3d 1068 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ) |
19 | 17, 18 | eqeltrrd 2689 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑦𝐷𝑥) ∈ ℝ) |
20 | 1 | xmeterval 22047 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑦𝐷𝑥) ∈ ℝ))) |
21 | 20 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑦𝐷𝑥) ∈ ℝ))) |
22 | 13, 14, 19, 21 | mpbir3and 1238 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∼ 𝑦) → 𝑦 ∼ 𝑥) |
23 | 14 | adantrr 749 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∈ 𝑋) |
24 | 1 | xmeterval 22047 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑦𝐷𝑧) ∈ ℝ))) |
25 | 24 | biimpa 500 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∼ 𝑧) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑦𝐷𝑧) ∈ ℝ)) |
26 | 25 | adantrl 748 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑦𝐷𝑧) ∈ ℝ)) |
27 | 26 | simp2d 1067 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑧 ∈ 𝑋) |
28 | | simpl 472 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋)) |
29 | 18 | adantrr 749 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥𝐷𝑦) ∈ ℝ) |
30 | 26 | simp3d 1068 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦𝐷𝑧) ∈ ℝ) |
31 | | rexadd 11937 |
. . . . . 6
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ (𝑦𝐷𝑧) ∈ ℝ) → ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) = ((𝑥𝐷𝑦) + (𝑦𝐷𝑧))) |
32 | | readdcl 9898 |
. . . . . 6
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ (𝑦𝐷𝑧) ∈ ℝ) → ((𝑥𝐷𝑦) + (𝑦𝐷𝑧)) ∈ ℝ) |
33 | 31, 32 | eqeltrd 2688 |
. . . . 5
⊢ (((𝑥𝐷𝑦) ∈ ℝ ∧ (𝑦𝐷𝑧) ∈ ℝ) → ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) ∈ ℝ) |
34 | 29, 30, 33 | syl2anc 691 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) ∈ ℝ) |
35 | 13 | adantrr 749 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑦 ∈ 𝑋) |
36 | | xmettri 21966 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑧) ≤ ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧))) |
37 | 28, 23, 27, 35, 36 | syl13anc 1320 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥𝐷𝑧) ≤ ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧))) |
38 | | xmetlecl 21961 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)) ∈ ℝ ∧ (𝑥𝐷𝑧) ≤ ((𝑥𝐷𝑦) +𝑒 (𝑦𝐷𝑧)))) → (𝑥𝐷𝑧) ∈ ℝ) |
39 | 28, 23, 27, 34, 37, 38 | syl122anc 1327 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥𝐷𝑧) ∈ ℝ) |
40 | 1 | xmeterval 22047 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥𝐷𝑧) ∈ ℝ))) |
41 | 40 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥𝐷𝑧) ∈ ℝ))) |
42 | 23, 27, 39, 41 | mpbir3and 1238 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∼ 𝑧) |
43 | | xmet0 21957 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐷𝑥) = 0) |
44 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
45 | 43, 44 | syl6eqel 2696 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥𝐷𝑥) ∈ ℝ) |
46 | 45 | ex 449 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 → (𝑥𝐷𝑥) ∈ ℝ)) |
47 | 46 | pm4.71rd 665 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ ((𝑥𝐷𝑥) ∈ ℝ ∧ 𝑥 ∈ 𝑋))) |
48 | | df-3an 1033 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (𝑥𝐷𝑥) ∈ ℝ)) |
49 | | anidm 674 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ↔ 𝑥 ∈ 𝑋) |
50 | 49 | anbi2ci 728 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (𝑥𝐷𝑥) ∈ ℝ) ↔ ((𝑥𝐷𝑥) ∈ ℝ ∧ 𝑥 ∈ 𝑋)) |
51 | 48, 50 | bitri 263 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ) ↔ ((𝑥𝐷𝑥) ∈ ℝ ∧ 𝑥 ∈ 𝑋)) |
52 | 47, 51 | syl6bbr 277 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ))) |
53 | 1 | xmeterval 22047 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (𝑥𝐷𝑥) ∈ ℝ))) |
54 | 52, 53 | bitr4d 270 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∼ 𝑥)) |
55 | 10, 22, 42, 54 | iserd 7655 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) |