| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vitali.1 | . . 3
⊢  ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} | 
| 2 | 1 | relopabiv 5830 | . 2
⊢ Rel ∼ | 
| 3 |  | simplr 769 | . . . 4
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ (0[,]1)) | 
| 4 |  | simpll 767 | . . . 4
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ (0[,]1)) | 
| 5 |  | unitssre 13539 | . . . . . . . . 9
⊢ (0[,]1)
⊆ ℝ | 
| 6 | 5 | sseli 3979 | . . . . . . . 8
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℝ) | 
| 7 | 6 | recnd 11289 | . . . . . . 7
⊢ (𝑢 ∈ (0[,]1) → 𝑢 ∈
ℂ) | 
| 8 | 7 | ad2antrr 726 | . . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑢 ∈ ℂ) | 
| 9 | 5 | sseli 3979 | . . . . . . . 8
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℝ) | 
| 10 | 9 | recnd 11289 | . . . . . . 7
⊢ (𝑣 ∈ (0[,]1) → 𝑣 ∈
ℂ) | 
| 11 | 10 | ad2antlr 727 | . . . . . 6
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → 𝑣 ∈ ℂ) | 
| 12 | 8, 11 | negsubdi2d 11636 | . . . . 5
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) = (𝑣 − 𝑢)) | 
| 13 |  | qnegcl 13008 | . . . . . 6
⊢ ((𝑢 − 𝑣) ∈ ℚ → -(𝑢 − 𝑣) ∈ ℚ) | 
| 14 | 13 | adantl 481 | . . . . 5
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → -(𝑢 − 𝑣) ∈ ℚ) | 
| 15 | 12, 14 | eqeltrrd 2842 | . . . 4
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → (𝑣 − 𝑢) ∈ ℚ) | 
| 16 | 3, 4, 15 | jca31 514 | . . 3
⊢ (((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ) → ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) | 
| 17 |  | oveq12 7440 | . . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥 − 𝑦) = (𝑢 − 𝑣)) | 
| 18 | 17 | eleq1d 2826 | . . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑣) ∈ ℚ)) | 
| 19 | 18, 1 | brab2a 5779 | . . 3
⊢ (𝑢 ∼ 𝑣 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) | 
| 20 |  | oveq12 7440 | . . . . 5
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑣 − 𝑢)) | 
| 21 | 20 | eleq1d 2826 | . . . 4
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑢) ∈ ℚ)) | 
| 22 | 21, 1 | brab2a 5779 | . . 3
⊢ (𝑣 ∼ 𝑢 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑣 − 𝑢) ∈ ℚ)) | 
| 23 | 16, 19, 22 | 3imtr4i 292 | . 2
⊢ (𝑢 ∼ 𝑣 → 𝑣 ∼ 𝑢) | 
| 24 |  | simpl 482 | . . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑣) | 
| 25 | 24, 19 | sylib 218 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) ∧ (𝑢 − 𝑣) ∈ ℚ)) | 
| 26 | 25 | simpld 494 | . . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1))) | 
| 27 | 26 | simpld 494 | . . 3
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ (0[,]1)) | 
| 28 |  | simpr 484 | . . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∼ 𝑤) | 
| 29 |  | oveq12 7440 | . . . . . . . 8
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑣 − 𝑤)) | 
| 30 | 29 | eleq1d 2826 | . . . . . . 7
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − 𝑤) ∈ ℚ)) | 
| 31 | 30, 1 | brab2a 5779 | . . . . . 6
⊢ (𝑣 ∼ 𝑤 ↔ ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) | 
| 32 | 28, 31 | sylib 218 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑣 − 𝑤) ∈ ℚ)) | 
| 33 | 32 | simpld 494 | . . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) | 
| 34 | 33 | simprd 495 | . . 3
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ (0[,]1)) | 
| 35 | 27, 7 | syl 17 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∈ ℂ) | 
| 36 | 25, 11 | syl 17 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑣 ∈ ℂ) | 
| 37 | 5, 34 | sselid 3981 | . . . . . 6
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℝ) | 
| 38 | 37 | recnd 11289 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑤 ∈ ℂ) | 
| 39 | 35, 36, 38 | npncand 11644 | . . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) = (𝑢 − 𝑤)) | 
| 40 | 25 | simprd 495 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑣) ∈ ℚ) | 
| 41 | 32 | simprd 495 | . . . . 5
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑣 − 𝑤) ∈ ℚ) | 
| 42 |  | qaddcl 13007 | . . . . 5
⊢ (((𝑢 − 𝑣) ∈ ℚ ∧ (𝑣 − 𝑤) ∈ ℚ) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) | 
| 43 | 40, 41, 42 | syl2anc 584 | . . . 4
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → ((𝑢 − 𝑣) + (𝑣 − 𝑤)) ∈ ℚ) | 
| 44 | 39, 43 | eqeltrrd 2842 | . . 3
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → (𝑢 − 𝑤) ∈ ℚ) | 
| 45 |  | oveq12 7440 | . . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → (𝑥 − 𝑦) = (𝑢 − 𝑤)) | 
| 46 | 45 | eleq1d 2826 | . . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑤) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑤) ∈ ℚ)) | 
| 47 | 46, 1 | brab2a 5779 | . . 3
⊢ (𝑢 ∼ 𝑤 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) ∧ (𝑢 − 𝑤) ∈ ℚ)) | 
| 48 | 27, 34, 44, 47 | syl21anbrc 1345 | . 2
⊢ ((𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤) → 𝑢 ∼ 𝑤) | 
| 49 | 7 | subidd 11608 | . . . . . 6
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) = 0) | 
| 50 |  | 0z 12624 | . . . . . . 7
⊢ 0 ∈
ℤ | 
| 51 |  | zq 12996 | . . . . . . 7
⊢ (0 ∈
ℤ → 0 ∈ ℚ) | 
| 52 | 50, 51 | ax-mp 5 | . . . . . 6
⊢ 0 ∈
ℚ | 
| 53 | 49, 52 | eqeltrdi 2849 | . . . . 5
⊢ (𝑢 ∈ (0[,]1) → (𝑢 − 𝑢) ∈ ℚ) | 
| 54 | 53 | adantr 480 | . . . 4
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) → (𝑢 − 𝑢) ∈ ℚ) | 
| 55 | 54 | pm4.71i 559 | . . 3
⊢ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) | 
| 56 |  | pm4.24 563 | . . 3
⊢ (𝑢 ∈ (0[,]1) ↔ (𝑢 ∈ (0[,]1) ∧ 𝑢 ∈
(0[,]1))) | 
| 57 |  | oveq12 7440 | . . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 − 𝑦) = (𝑢 − 𝑢)) | 
| 58 | 57 | eleq1d 2826 | . . . 4
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑢 − 𝑢) ∈ ℚ)) | 
| 59 | 58, 1 | brab2a 5779 | . . 3
⊢ (𝑢 ∼ 𝑢 ↔ ((𝑢 ∈ (0[,]1) ∧ 𝑢 ∈ (0[,]1)) ∧ (𝑢 − 𝑢) ∈ ℚ)) | 
| 60 | 55, 56, 59 | 3bitr4i 303 | . 2
⊢ (𝑢 ∈ (0[,]1) ↔ 𝑢 ∼ 𝑢) | 
| 61 | 2, 23, 48, 60 | iseri 8772 | 1
⊢  ∼ Er
(0[,]1) |