Step | Hyp | Ref
| Expression |
1 | | vitali.1 |
. . 3
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
2 | 1 | relopabiv 5690 |
. 2
⊢ Rel ∼ |
3 | | simplr 769 |
. . . 4
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ (0[,]1)) |
4 | | simpll 767 |
. . . 4
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ (0[,]1)) |
5 | | unitssre 13087 |
. . . . . . . . 9
⊢ (0[,]1)
⊆ ℝ |
6 | 5 | sseli 3896 |
. . . . . . . 8
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℝ) |
7 | 6 | recnd 10861 |
. . . . . . 7
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℂ) |
8 | 7 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ ℂ) |
9 | 5 | sseli 3896 |
. . . . . . . 8
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℝ) |
10 | 9 | recnd 10861 |
. . . . . . 7
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℂ) |
11 | 10 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ ℂ) |
12 | 8, 11 | negsubdi2d 11205 |
. . . . 5
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) = (𝑣 − 𝑢)) |
13 | | qnegcl 12562 |
. . . . . 6
⊢ ((𝑢 − 𝑣) ∈ ℚ → -(𝑢 − 𝑣) ∈ ℚ) |
14 | 13 | adantl 485 |
. . . . 5
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) ∈ ℚ) |
15 | 12, 14 | eqeltrrd 2839 |
. . . 4
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → (𝑣 − 𝑢) ∈ ℚ) |
16 | 3, 4, 15 | jca31 518 |
. . 3
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) |
17 | | oveq12 7222 |
. . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 − 𝑦) = (𝑢 − 𝑣)) |
18 | 17 | eleq1d 2822 |
. . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑣) ∈ ℚ)) |
19 | 18, 1 | brab2a 5641 |
. . 3
⊢ (𝑢 ∼ 𝑣 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) |
20 | | oveq12 7222 |
. . . . 5
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑣 − 𝑢)) |
21 | 20 | eleq1d 2822 |
. . . 4
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑢) ∈ ℚ)) |
22 | 21, 1 | brab2a 5641 |
. . 3
⊢ (𝑣 ∼ 𝑢 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) |
23 | 16, 19, 22 | 3imtr4i 295 |
. 2
⊢ (𝑢 ∼ 𝑣 → 𝑣 ∼ 𝑢) |
24 | | simpl 486 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑣) |
25 | 24, 19 | sylib 221 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) |
26 | 25 | simpld 498 |
. . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1))) |
27 | 26 | simpld 498 |
. . 3
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ (0[,]1)) |
28 | | simpr 488 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∼ 𝑤) |
29 | | oveq12 7222 |
. . . . . . . 8
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑣 − 𝑤)) |
30 | 29 | eleq1d 2822 |
. . . . . . 7
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑤) ∈ ℚ)) |
31 | 30, 1 | brab2a 5641 |
. . . . . 6
⊢ (𝑣 ∼ 𝑤 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) |
32 | 28, 31 | sylib 221 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) |
33 | 32 | simpld 498 |
. . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) |
34 | 33 | simprd 499 |
. . 3
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ (0[,]1)) |
35 | 27, 7 | syl 17 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ ℂ) |
36 | 25, 11 | syl 17 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∈ ℂ) |
37 | 5, 34 | sseldi 3899 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℝ) |
38 | 37 | recnd 10861 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℂ) |
39 | 35, 36, 38 | npncand 11213 |
. . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) = (𝑢 − 𝑤)) |
40 | 25 | simprd 499 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑣) ∈ ℚ) |
41 | 32 | simprd 499 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 − 𝑤) ∈ ℚ) |
42 | | qaddcl 12561 |
. . . . 5
⊢ (((𝑢 − 𝑣) ∈ ℚ ∧ (𝑣 − 𝑤) ∈ ℚ) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) |
43 | 40, 41, 42 | syl2anc 587 |
. . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) |
44 | 39, 43 | eqeltrrd 2839 |
. . 3
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑤) ∈ ℚ) |
45 | | oveq12 7222 |
. . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑢 − 𝑤)) |
46 | 45 | eleq1d 2822 |
. . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑤) ∈ ℚ)) |
47 | 46, 1 | brab2a 5641 |
. . 3
⊢ (𝑢 ∼ 𝑤 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑢 − 𝑤) ∈ ℚ)) |
48 | 27, 34, 44, 47 | syl21anbrc 1346 |
. 2
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑤) |
49 | 7 | subidd 11177 |
. . . . . 6
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) = 0) |
50 | | 0z 12187 |
. . . . . . 7
⊢ 0 ∈
ℤ |
51 | | zq 12550 |
. . . . . . 7
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
52 | 50, 51 | ax-mp 5 |
. . . . . 6
⊢ 0 ∈
ℚ |
53 | 49, 52 | eqeltrdi 2846 |
. . . . 5
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) ∈ ℚ) |
54 | 53 | adantr 484 |
. . . 4
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) → (𝑢 − 𝑢) ∈ ℚ) |
55 | 54 | pm4.71i 563 |
. . 3
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) |
56 | | pm4.24 567 |
. . 3
⊢ (𝑢 ∈ (0[,]1) ↔ (𝑢 ∈ (0[,]1) ∧ 𝑢 ∈
(0[,]1))) |
57 | | oveq12 7222 |
. . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑢 − 𝑢)) |
58 | 57 | eleq1d 2822 |
. . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑢) ∈ ℚ)) |
59 | 58, 1 | brab2a 5641 |
. . 3
⊢ (𝑢 ∼ 𝑢 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) |
60 | 55, 56, 59 | 3bitr4i 306 |
. 2
⊢ (𝑢 ∈ (0[,]1) ↔ 𝑢 ∼ 𝑢) |
61 | 2, 23, 48, 60 | iseri 8418 |
1
⊢ ∼ Er
(0[,]1) |