Metamath Proof Explorer

Theorem vitalilem1

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014) (Proof shortened by AV, 1-May-2021)

Ref Expression
Hypothesis vitali.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
Assertion vitalilem1 ∼ Er ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 vitali.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
2 1 relopabiv ⊢ Rel ∼
3 simplr ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → 𝑣 ∈ ( 0 [,] 1 ) )
4 simpll ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → 𝑢 ∈ ( 0 [,] 1 ) )
5 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
6 5 sseli ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → 𝑢 ∈ ℝ )
7 6 recnd ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → 𝑢 ∈ ℂ )
8 7 ad2antrr ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → 𝑢 ∈ ℂ )
9 5 sseli ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → 𝑣 ∈ ℝ )
10 9 recnd ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → 𝑣 ∈ ℂ )
11 10 ad2antlr ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → 𝑣 ∈ ℂ )
12 8 11 negsubdi2d ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → - ( 𝑢 − 𝑣 ) = ( 𝑣 − 𝑢 ) )
13 qnegcl ⊢ ( ( 𝑢 − 𝑣 ) ∈ ℚ → - ( 𝑢 − 𝑣 ) ∈ ℚ )
14 13 adantl ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → - ( 𝑢 − 𝑣 ) ∈ ℚ )
15 12 14 eqeltrrd ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → ( 𝑣 − 𝑢 ) ∈ ℚ )
16 3 4 15 jca31 ⊢ ( ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) → ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − 𝑢 ) ∈ ℚ ) )
17 oveq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑣 ) )
18 17 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑢 − 𝑣 ) ∈ ℚ ) )
19 18 1 brab2a ⊢ ( 𝑢 ∼ 𝑣 ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) )
20 oveq12 ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝑥 − 𝑦 ) = ( 𝑣 − 𝑢 ) )
21 20 eleq1d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑣 − 𝑢 ) ∈ ℚ ) )
22 21 1 brab2a ⊢ ( 𝑣 ∼ 𝑢 ↔ ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − 𝑢 ) ∈ ℚ ) )
23 16 19 22 3imtr4i ⊢ ( 𝑢 ∼ 𝑣 → 𝑣 ∼ 𝑢 )
24 simpl ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∼ 𝑣 )
25 24 19 sylib ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) )
26 25 simpld ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) )
27 26 simpld ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∈ ( 0 [,] 1 ) )
28 simpr ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑣 ∼ 𝑤 )
29 oveq12 ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝑥 − 𝑦 ) = ( 𝑣 − 𝑤 ) )
30 29 eleq1d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑣 − 𝑤 ) ∈ ℚ ) )
31 30 1 brab2a ⊢ ( 𝑣 ∼ 𝑤 ↔ ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − 𝑤 ) ∈ ℚ ) )
32 28 31 sylib ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − 𝑤 ) ∈ ℚ ) )
33 32 simpld ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) )
34 33 simprd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑤 ∈ ( 0 [,] 1 ) )
35 27 7 syl ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∈ ℂ )
36 25 11 syl ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑣 ∈ ℂ )
37 5 34 sselid ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑤 ∈ ℝ )
38 37 recnd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑤 ∈ ℂ )
39 35 36 38 npncand ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑢 − 𝑣 ) + ( 𝑣 − 𝑤 ) ) = ( 𝑢 − 𝑤 ) )
40 25 simprd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑢 − 𝑣 ) ∈ ℚ )
41 32 simprd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑣 − 𝑤 ) ∈ ℚ )
42 qaddcl ⊢ ( ( ( 𝑢 − 𝑣 ) ∈ ℚ ∧ ( 𝑣 − 𝑤 ) ∈ ℚ ) → ( ( 𝑢 − 𝑣 ) + ( 𝑣 − 𝑤 ) ) ∈ ℚ )
43 40 41 42 syl2anc ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑢 − 𝑣 ) + ( 𝑣 − 𝑤 ) ) ∈ ℚ )
44 39 43 eqeltrrd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑢 − 𝑤 ) ∈ ℚ )
45 oveq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑤 ) → ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑤 ) )
46 45 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑢 − 𝑤 ) ∈ ℚ ) )
47 46 1 brab2a ⊢ ( 𝑢 ∼ 𝑤 ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑤 ) ∈ ℚ ) )
48 27 34 44 47 syl21anbrc ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∼ 𝑤 )
49 7 subidd ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → ( 𝑢 − 𝑢 ) = 0 )
50 0z ⊢ 0 ∈ ℤ
51 zq ⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
52 50 51 ax-mp ⊢ 0 ∈ ℚ
53 49 52 eqeltrdi ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → ( 𝑢 − 𝑢 ) ∈ ℚ )
54 53 adantr ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) → ( 𝑢 − 𝑢 ) ∈ ℚ )
55 54 pm4.71i ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑢 ) ∈ ℚ ) )
56 pm4.24 ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) ↔ ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) )
57 oveq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑢 ) )
58 57 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑢 − 𝑢 ) ∈ ℚ ) )
59 58 1 brab2a ⊢ ( 𝑢 ∼ 𝑢 ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑢 ) ∈ ℚ ) )
60 55 56 59 3bitr4i ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) ↔ 𝑢 ∼ 𝑢 )
61 2 23 48 60 iseri ⊢ ∼ Er ( 0 [,] 1 )