Step | Hyp | Ref
| Expression |
1 | | vitali.1 |
. . . . 5
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
2 | 1 | relopabi 5167 |
. . . 4
⊢ Rel ∼ |
3 | 2 | a1i 11 |
. . 3
⊢ (⊤
→ Rel ∼ ) |
4 | | simplr 788 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ (0[,]1)) |
5 | | simpll 786 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ (0[,]1)) |
6 | | unitssre 12190 |
. . . . . . . . . . 11
⊢ (0[,]1)
⊆ ℝ |
7 | 6 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℝ) |
8 | 7 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℂ) |
9 | 8 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ ℂ) |
10 | 6 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℝ) |
11 | 10 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℂ) |
12 | 11 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ ℂ) |
13 | 9, 12 | negsubdi2d 10287 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) = (𝑣 − 𝑢)) |
14 | | qnegcl 11681 |
. . . . . . . 8
⊢ ((𝑢 − 𝑣) ∈ ℚ → -(𝑢 − 𝑣) ∈ ℚ) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) ∈ ℚ) |
16 | 13, 15 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → (𝑣 − 𝑢) ∈ ℚ) |
17 | 4, 5, 16 | jca31 555 |
. . . . 5
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) |
18 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 − 𝑦) = (𝑢 − 𝑣)) |
19 | 18 | eleq1d 2672 |
. . . . . 6
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑣) ∈ ℚ)) |
20 | 19, 1 | brab2ga 5117 |
. . . . 5
⊢ (𝑢 ∼ 𝑣 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) |
21 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑣 − 𝑢)) |
22 | 21 | eleq1d 2672 |
. . . . . 6
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑢) ∈ ℚ)) |
23 | 22, 1 | brab2ga 5117 |
. . . . 5
⊢ (𝑣 ∼ 𝑢 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) |
24 | 17, 20, 23 | 3imtr4i 280 |
. . . 4
⊢ (𝑢 ∼ 𝑣 → 𝑣 ∼ 𝑢) |
25 | 24 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑢
∼
𝑣) → 𝑣 ∼ 𝑢) |
26 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑣) |
27 | 26, 20 | sylib 207 |
. . . . . . . 8
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) |
28 | 27 | simpld 474 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1))) |
29 | 28 | simpld 474 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ (0[,]1)) |
30 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∼ 𝑤) |
31 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑣 − 𝑤)) |
32 | 31 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑤) ∈ ℚ)) |
33 | 32, 1 | brab2ga 5117 |
. . . . . . . . 9
⊢ (𝑣 ∼ 𝑤 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) |
34 | 30, 33 | sylib 207 |
. . . . . . . 8
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) |
35 | 34 | simpld 474 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) |
36 | 35 | simprd 478 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ (0[,]1)) |
37 | 29, 36 | jca 553 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) |
38 | 29, 8 | syl 17 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ ℂ) |
39 | 27, 12 | syl 17 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∈ ℂ) |
40 | 6, 36 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℝ) |
41 | 40 | recnd 9947 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℂ) |
42 | 38, 39, 41 | npncand 10295 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) = (𝑢 − 𝑤)) |
43 | 27 | simprd 478 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑣) ∈ ℚ) |
44 | 34 | simprd 478 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 − 𝑤) ∈ ℚ) |
45 | | qaddcl 11680 |
. . . . . . 7
⊢ (((𝑢 − 𝑣) ∈ ℚ ∧ (𝑣 − 𝑤) ∈ ℚ) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) |
46 | 43, 44, 45 | syl2anc 691 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) |
47 | 42, 46 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑤) ∈ ℚ) |
48 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑢 − 𝑤)) |
49 | 48 | eleq1d 2672 |
. . . . . 6
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑤) ∈ ℚ)) |
50 | 49, 1 | brab2ga 5117 |
. . . . 5
⊢ (𝑢 ∼ 𝑤 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑢 − 𝑤) ∈ ℚ)) |
51 | 37, 47, 50 | sylanbrc 695 |
. . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑤) |
52 | 51 | adantl 481 |
. . 3
⊢
((⊤ ∧ (𝑢
∼
𝑣 ∧ 𝑣 ∼ 𝑤)) → 𝑢 ∼ 𝑤) |
53 | 8 | subidd 10259 |
. . . . . . . 8
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) = 0) |
54 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
55 | | zq 11670 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ∈
ℚ |
57 | 53, 56 | syl6eqel 2696 |
. . . . . . 7
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) ∈ ℚ) |
58 | 57 | adantr 480 |
. . . . . 6
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) → (𝑢 − 𝑢) ∈ ℚ) |
59 | 58 | pm4.71i 662 |
. . . . 5
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) |
60 | | pm4.24 673 |
. . . . 5
⊢ (𝑢 ∈ (0[,]1) ↔ (𝑢 ∈ (0[,]1) ∧ 𝑢 ∈
(0[,]1))) |
61 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑢 − 𝑢)) |
62 | 61 | eleq1d 2672 |
. . . . . 6
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑢) ∈ ℚ)) |
63 | 62, 1 | brab2ga 5117 |
. . . . 5
⊢ (𝑢 ∼ 𝑢 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) |
64 | 59, 60, 63 | 3bitr4i 291 |
. . . 4
⊢ (𝑢 ∈ (0[,]1) ↔ 𝑢 ∼ 𝑢) |
65 | 64 | a1i 11 |
. . 3
⊢ (⊤
→ (𝑢 ∈ (0[,]1)
↔ 𝑢 ∼ 𝑢)) |
66 | 3, 25, 52, 65 | iserd 7655 |
. 2
⊢ (⊤
→ ∼ Er
(0[,]1)) |
67 | 66 | trud 1484 |
1
⊢ ∼ Er
(0[,]1) |