Step | Hyp | Ref
| Expression |
1 | | vitali.1 |
. . . . 5
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
2 | 1 | relopabi 5245 |
. . . 4
⊢ Rel ∼ |
3 | 2 | a1i 11 |
. . 3
⊢ (⊤
→ Rel ∼ ) |
4 | | simplr 792 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ (0[,]1)) |
5 | | simpll 790 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ (0[,]1)) |
6 | | unitssre 12319 |
. . . . . . . . . . 11
⊢ (0[,]1)
⊆ ℝ |
7 | 6 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℝ) |
8 | 7 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℂ) |
9 | 8 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ ℂ) |
10 | 6 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℝ) |
11 | 10 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℂ) |
12 | 11 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ ℂ) |
13 | 9, 12 | negsubdi2d 10408 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) = (𝑣 − 𝑢)) |
14 | | qnegcl 11805 |
. . . . . . . 8
⊢ ((𝑢 − 𝑣) ∈ ℚ → -(𝑢 − 𝑣) ∈ ℚ) |
15 | 14 | adantl 482 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) ∈ ℚ) |
16 | 13, 15 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → (𝑣 − 𝑢) ∈ ℚ) |
17 | 4, 5, 16 | jca31 557 |
. . . . 5
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) |
18 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 − 𝑦) = (𝑢 − 𝑣)) |
19 | 18 | eleq1d 2686 |
. . . . . 6
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑣) ∈ ℚ)) |
20 | 19, 1 | brab2a 5194 |
. . . . 5
⊢ (𝑢 ∼ 𝑣 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) |
21 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑣 − 𝑢)) |
22 | 21 | eleq1d 2686 |
. . . . . 6
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑢) ∈ ℚ)) |
23 | 22, 1 | brab2a 5194 |
. . . . 5
⊢ (𝑣 ∼ 𝑢 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) |
24 | 17, 20, 23 | 3imtr4i 281 |
. . . 4
⊢ (𝑢 ∼ 𝑣 → 𝑣 ∼ 𝑢) |
25 | 24 | adantl 482 |
. . 3
⊢
((⊤ ∧ 𝑢
∼
𝑣) → 𝑣 ∼ 𝑢) |
26 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑣) |
27 | 26, 20 | sylib 208 |
. . . . . . . 8
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) |
28 | 27 | simpld 475 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1))) |
29 | 28 | simpld 475 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ (0[,]1)) |
30 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∼ 𝑤) |
31 | | oveq12 6659 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑣 − 𝑤)) |
32 | 31 | eleq1d 2686 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑤) ∈ ℚ)) |
33 | 32, 1 | brab2a 5194 |
. . . . . . . . 9
⊢ (𝑣 ∼ 𝑤 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) |
34 | 30, 33 | sylib 208 |
. . . . . . . 8
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) |
35 | 34 | simpld 475 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) |
36 | 35 | simprd 479 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ (0[,]1)) |
37 | 29, 36 | jca 554 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) |
38 | 29, 8 | syl 17 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ ℂ) |
39 | 27, 12 | syl 17 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∈ ℂ) |
40 | 6, 36 | sseldi 3601 |
. . . . . . . 8
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℝ) |
41 | 40 | recnd 10068 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℂ) |
42 | 38, 39, 41 | npncand 10416 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) = (𝑢 − 𝑤)) |
43 | 27 | simprd 479 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑣) ∈ ℚ) |
44 | 34 | simprd 479 |
. . . . . . 7
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 − 𝑤) ∈ ℚ) |
45 | | qaddcl 11804 |
. . . . . . 7
⊢ (((𝑢 − 𝑣) ∈ ℚ ∧ (𝑣 − 𝑤) ∈ ℚ) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) |
46 | 43, 44, 45 | syl2anc 693 |
. . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) |
47 | 42, 46 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑤) ∈ ℚ) |
48 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑢 − 𝑤)) |
49 | 48 | eleq1d 2686 |
. . . . . 6
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑤) ∈ ℚ)) |
50 | 49, 1 | brab2a 5194 |
. . . . 5
⊢ (𝑢 ∼ 𝑤 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑢 − 𝑤) ∈ ℚ)) |
51 | 37, 47, 50 | sylanbrc 698 |
. . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑤) |
52 | 51 | adantl 482 |
. . 3
⊢
((⊤ ∧ (𝑢
∼
𝑣 ∧ 𝑣 ∼ 𝑤)) → 𝑢 ∼ 𝑤) |
53 | 8 | subidd 10380 |
. . . . . . . 8
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) = 0) |
54 | | 0z 11388 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
55 | | zq 11794 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . 8
⊢ 0 ∈
ℚ |
57 | 53, 56 | syl6eqel 2709 |
. . . . . . 7
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) ∈ ℚ) |
58 | 57 | adantr 481 |
. . . . . 6
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) → (𝑢 − 𝑢) ∈ ℚ) |
59 | 58 | pm4.71i 664 |
. . . . 5
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) |
60 | | pm4.24 675 |
. . . . 5
⊢ (𝑢 ∈ (0[,]1) ↔ (𝑢 ∈ (0[,]1) ∧ 𝑢 ∈
(0[,]1))) |
61 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑢 − 𝑢)) |
62 | 61 | eleq1d 2686 |
. . . . . 6
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑢) ∈ ℚ)) |
63 | 62, 1 | brab2a 5194 |
. . . . 5
⊢ (𝑢 ∼ 𝑢 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) |
64 | 59, 60, 63 | 3bitr4i 292 |
. . . 4
⊢ (𝑢 ∈ (0[,]1) ↔ 𝑢 ∼ 𝑢) |
65 | 64 | a1i 11 |
. . 3
⊢ (⊤
→ (𝑢 ∈ (0[,]1)
↔ 𝑢 ∼ 𝑢)) |
66 | 3, 25, 52, 65 | iserd 7768 |
. 2
⊢ (⊤
→ ∼ Er
(0[,]1)) |
67 | 66 | trud 1493 |
1
⊢ ∼ Er
(0[,]1) |