Step | Hyp | Ref
| Expression |
1 | | 0re 10666 |
. . . . . 6
⊢ 0 ∈
ℝ |
2 | | 1re 10664 |
. . . . . 6
⊢ 1 ∈
ℝ |
3 | 1, 2 | ifcli 4460 |
. . . . 5
⊢ if(𝑥 = 𝑦, 0, 1) ∈ ℝ |
4 | 3 | rgen2w 3081 |
. . . 4
⊢
∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 if(𝑥 = 𝑦, 0, 1) ∈ ℝ |
5 | | dscmet.1 |
. . . . 5
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1)) |
6 | 5 | fmpo 7763 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 if(𝑥 = 𝑦, 0, 1) ∈ ℝ ↔ 𝐷:(𝑋 × 𝑋)⟶ℝ) |
7 | 4, 6 | mpbi 233 |
. . 3
⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ |
8 | | equequ1 2033 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 ↔ 𝑤 = 𝑦)) |
9 | 8 | ifbid 4436 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → if(𝑥 = 𝑦, 0, 1) = if(𝑤 = 𝑦, 0, 1)) |
10 | | equequ2 2034 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (𝑤 = 𝑦 ↔ 𝑤 = 𝑣)) |
11 | 10 | ifbid 4436 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → if(𝑤 = 𝑦, 0, 1) = if(𝑤 = 𝑣, 0, 1)) |
12 | | 0nn0 11934 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
13 | | 1nn0 11935 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
14 | 12, 13 | ifcli 4460 |
. . . . . . . . 9
⊢ if(𝑤 = 𝑣, 0, 1) ∈
ℕ0 |
15 | 14 | elexi 3428 |
. . . . . . . 8
⊢ if(𝑤 = 𝑣, 0, 1) ∈ V |
16 | 9, 11, 5, 15 | ovmpo 7298 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑤𝐷𝑣) = if(𝑤 = 𝑣, 0, 1)) |
17 | 16 | eqeq1d 2761 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ((𝑤𝐷𝑣) = 0 ↔ if(𝑤 = 𝑣, 0, 1) = 0)) |
18 | | iffalse 4422 |
. . . . . . . . . 10
⊢ (¬
𝑤 = 𝑣 → if(𝑤 = 𝑣, 0, 1) = 1) |
19 | | ax-1ne0 10629 |
. . . . . . . . . . 11
⊢ 1 ≠
0 |
20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ (¬
𝑤 = 𝑣 → 1 ≠ 0) |
21 | 18, 20 | eqnetrd 3016 |
. . . . . . . . 9
⊢ (¬
𝑤 = 𝑣 → if(𝑤 = 𝑣, 0, 1) ≠ 0) |
22 | 21 | neneqd 2954 |
. . . . . . . 8
⊢ (¬
𝑤 = 𝑣 → ¬ if(𝑤 = 𝑣, 0, 1) = 0) |
23 | 22 | con4i 114 |
. . . . . . 7
⊢ (if(𝑤 = 𝑣, 0, 1) = 0 → 𝑤 = 𝑣) |
24 | | iftrue 4419 |
. . . . . . 7
⊢ (𝑤 = 𝑣 → if(𝑤 = 𝑣, 0, 1) = 0) |
25 | 23, 24 | impbii 212 |
. . . . . 6
⊢ (if(𝑤 = 𝑣, 0, 1) = 0 ↔ 𝑤 = 𝑣) |
26 | 17, 25 | bitrdi 290 |
. . . . 5
⊢ ((𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣)) |
27 | 12, 13 | ifcli 4460 |
. . . . . . . . . . 11
⊢ if(𝑢 = 𝑤, 0, 1) ∈
ℕ0 |
28 | 12, 13 | ifcli 4460 |
. . . . . . . . . . 11
⊢ if(𝑢 = 𝑣, 0, 1) ∈
ℕ0 |
29 | 27, 28 | nn0addcli 11956 |
. . . . . . . . . 10
⊢ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈
ℕ0 |
30 | | elnn0 11921 |
. . . . . . . . . 10
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ0 ↔
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ ∨ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0)) |
31 | 29, 30 | mpbi 233 |
. . . . . . . . 9
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ ∨ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0) |
32 | | breq1 5028 |
. . . . . . . . . . . 12
⊢ (0 =
if(𝑤 = 𝑣, 0, 1) → (0 ≤ 1 ↔ if(𝑤 = 𝑣, 0, 1) ≤ 1)) |
33 | | breq1 5028 |
. . . . . . . . . . . 12
⊢ (1 =
if(𝑤 = 𝑣, 0, 1) → (1 ≤ 1 ↔ if(𝑤 = 𝑣, 0, 1) ≤ 1)) |
34 | | 0le1 11186 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
35 | 2 | leidi 11197 |
. . . . . . . . . . . 12
⊢ 1 ≤
1 |
36 | 32, 33, 34, 35 | keephyp 4484 |
. . . . . . . . . . 11
⊢ if(𝑤 = 𝑣, 0, 1) ≤ 1 |
37 | | nnge1 11687 |
. . . . . . . . . . 11
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ → 1 ≤
(if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
38 | 14 | nn0rei 11930 |
. . . . . . . . . . . 12
⊢ if(𝑤 = 𝑣, 0, 1) ∈ ℝ |
39 | 29 | nn0rei 11930 |
. . . . . . . . . . . 12
⊢ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℝ |
40 | 38, 2, 39 | letri 10792 |
. . . . . . . . . . 11
⊢
((if(𝑤 = 𝑣, 0, 1) ≤ 1 ∧ 1 ≤
(if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
41 | 36, 37, 40 | sylancr 591 |
. . . . . . . . . 10
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
42 | 27 | nn0ge0i 11946 |
. . . . . . . . . . . . 13
⊢ 0 ≤
if(𝑢 = 𝑤, 0, 1) |
43 | 28 | nn0ge0i 11946 |
. . . . . . . . . . . . 13
⊢ 0 ≤
if(𝑢 = 𝑣, 0, 1) |
44 | 27 | nn0rei 11930 |
. . . . . . . . . . . . . 14
⊢ if(𝑢 = 𝑤, 0, 1) ∈ ℝ |
45 | 28 | nn0rei 11930 |
. . . . . . . . . . . . . 14
⊢ if(𝑢 = 𝑣, 0, 1) ∈ ℝ |
46 | 44, 45 | add20i 11206 |
. . . . . . . . . . . . 13
⊢ ((0 ≤
if(𝑢 = 𝑤, 0, 1) ∧ 0 ≤ if(𝑢 = 𝑣, 0, 1)) → ((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 ↔ (if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0))) |
47 | 42, 43, 46 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 ↔ (if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0)) |
48 | | equequ2 2034 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑤)) |
49 | 48 | ifbid 4436 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑤 → if(𝑢 = 𝑣, 0, 1) = if(𝑢 = 𝑤, 0, 1)) |
50 | 49 | eqeq1d 2761 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑤 → (if(𝑢 = 𝑣, 0, 1) = 0 ↔ if(𝑢 = 𝑤, 0, 1) = 0)) |
51 | 50, 48 | bibi12d 350 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → ((if(𝑢 = 𝑣, 0, 1) = 0 ↔ 𝑢 = 𝑣) ↔ (if(𝑢 = 𝑤, 0, 1) = 0 ↔ 𝑢 = 𝑤))) |
52 | | equequ1 2033 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑢 → (𝑤 = 𝑣 ↔ 𝑢 = 𝑣)) |
53 | 52 | ifbid 4436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑢 → if(𝑤 = 𝑣, 0, 1) = if(𝑢 = 𝑣, 0, 1)) |
54 | 53 | eqeq1d 2761 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑢 → (if(𝑤 = 𝑣, 0, 1) = 0 ↔ if(𝑢 = 𝑣, 0, 1) = 0)) |
55 | 54, 52 | bibi12d 350 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑢 → ((if(𝑤 = 𝑣, 0, 1) = 0 ↔ 𝑤 = 𝑣) ↔ (if(𝑢 = 𝑣, 0, 1) = 0 ↔ 𝑢 = 𝑣))) |
56 | 55, 25 | chvarvv 2006 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝑢 = 𝑣, 0, 1) = 0 ↔ 𝑢 = 𝑣) |
57 | 51, 56 | chvarvv 2006 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑢 = 𝑤, 0, 1) = 0 ↔ 𝑢 = 𝑤) |
58 | | eqtr2 2780 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑤 ∧ 𝑢 = 𝑣) → 𝑤 = 𝑣) |
59 | 57, 56, 58 | syl2anb 601 |
. . . . . . . . . . . . . 14
⊢
((if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0) → 𝑤 = 𝑣) |
60 | 59 | iftrued 4421 |
. . . . . . . . . . . . 13
⊢
((if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0) → if(𝑤 = 𝑣, 0, 1) = 0) |
61 | 1 | leidi 11197 |
. . . . . . . . . . . . 13
⊢ 0 ≤
0 |
62 | 60, 61 | eqbrtrdi 5064 |
. . . . . . . . . . . 12
⊢
((if(𝑢 = 𝑤, 0, 1) = 0 ∧ if(𝑢 = 𝑣, 0, 1) = 0) → if(𝑤 = 𝑣, 0, 1) ≤ 0) |
63 | 47, 62 | sylbi 220 |
. . . . . . . . . . 11
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 → if(𝑤 = 𝑣, 0, 1) ≤ 0) |
64 | | id 22 |
. . . . . . . . . . 11
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 → (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0) |
65 | 63, 64 | breqtrrd 5053 |
. . . . . . . . . 10
⊢
((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0 → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
66 | 41, 65 | jaoi 855 |
. . . . . . . . 9
⊢
(((if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) ∈ ℕ ∨ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1)) = 0) → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
67 | 31, 66 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → if(𝑤 = 𝑣, 0, 1) ≤ (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
68 | 16 | adantl 486 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑤𝐷𝑣) = if(𝑤 = 𝑣, 0, 1)) |
69 | | eqeq12 2773 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → (𝑥 = 𝑦 ↔ 𝑢 = 𝑤)) |
70 | 69 | ifbid 4436 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → if(𝑥 = 𝑦, 0, 1) = if(𝑢 = 𝑤, 0, 1)) |
71 | 27 | elexi 3428 |
. . . . . . . . . . 11
⊢ if(𝑢 = 𝑤, 0, 1) ∈ V |
72 | 70, 5, 71 | ovmpoa 7293 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢𝐷𝑤) = if(𝑢 = 𝑤, 0, 1)) |
73 | 72 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢𝐷𝑤) = if(𝑢 = 𝑤, 0, 1)) |
74 | | eqeq12 2773 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 = 𝑦 ↔ 𝑢 = 𝑣)) |
75 | 74 | ifbid 4436 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → if(𝑥 = 𝑦, 0, 1) = if(𝑢 = 𝑣, 0, 1)) |
76 | 28 | elexi 3428 |
. . . . . . . . . . 11
⊢ if(𝑢 = 𝑣, 0, 1) ∈ V |
77 | 75, 5, 76 | ovmpoa 7293 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢𝐷𝑣) = if(𝑢 = 𝑣, 0, 1)) |
78 | 77 | adantrl 716 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢𝐷𝑣) = if(𝑢 = 𝑣, 0, 1)) |
79 | 73, 78 | oveq12d 7161 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)) = (if(𝑢 = 𝑤, 0, 1) + if(𝑢 = 𝑣, 0, 1))) |
80 | 67, 68, 79 | 3brtr4d 5057 |
. . . . . . 7
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))) |
81 | 80 | expcom 418 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢 ∈ 𝑋 → (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))) |
82 | 81 | ralrimiv 3110 |
. . . . 5
⊢ ((𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∀𝑢 ∈ 𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))) |
83 | 26, 82 | jca 516 |
. . . 4
⊢ ((𝑤 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢 ∈ 𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))) |
84 | 83 | rgen2 3130 |
. . 3
⊢
∀𝑤 ∈
𝑋 ∀𝑣 ∈ 𝑋 (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢 ∈ 𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣))) |
85 | 7, 84 | pm3.2i 475 |
. 2
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑤 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢 ∈ 𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))) |
86 | | ismet 23010 |
. 2
⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑤 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (((𝑤𝐷𝑣) = 0 ↔ 𝑤 = 𝑣) ∧ ∀𝑢 ∈ 𝑋 (𝑤𝐷𝑣) ≤ ((𝑢𝐷𝑤) + (𝑢𝐷𝑣)))))) |
87 | 85, 86 | mpbiri 261 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋)) |