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 19 birani ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑣 ) ∈ ℚ ) )
25 24 simpld ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) )
26 25 simpld ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∈ ( 0 [,] 1 ) )
27 oveq12 ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( 𝑥 − 𝑦 ) = ( 𝑣 − 𝑤 ) )
28 27 eleq1d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑣 − 𝑤 ) ∈ ℚ ) )
29 28 1 brab2a ⊢ ( 𝑣 ∼ 𝑤 ↔ ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − 𝑤 ) ∈ ℚ ) )
30 29 bilani ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − 𝑤 ) ∈ ℚ ) )
31 30 simpld ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑣 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) )
32 31 simprd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑤 ∈ ( 0 [,] 1 ) )
33 26 7 syl ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∈ ℂ )
34 24 11 syl ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑣 ∈ ℂ )
35 5 32 sselid ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑤 ∈ ℝ )
36 35 recnd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑤 ∈ ℂ )
37 33 34 36 npncand ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑢 − 𝑣 ) + ( 𝑣 − 𝑤 ) ) = ( 𝑢 − 𝑤 ) )
38 24 simprd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑢 − 𝑣 ) ∈ ℚ )
39 30 simprd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑣 − 𝑤 ) ∈ ℚ )
40 qaddcl ⊢ ( ( ( 𝑢 − 𝑣 ) ∈ ℚ ∧ ( 𝑣 − 𝑤 ) ∈ ℚ ) → ( ( 𝑢 − 𝑣 ) + ( 𝑣 − 𝑤 ) ) ∈ ℚ )
41 38 39 40 syl2anc ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( ( 𝑢 − 𝑣 ) + ( 𝑣 − 𝑤 ) ) ∈ ℚ )
42 37 41 eqeltrrd ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → ( 𝑢 − 𝑤 ) ∈ ℚ )
43 oveq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑤 ) → ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑤 ) )
44 43 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑢 − 𝑤 ) ∈ ℚ ) )
45 44 1 brab2a ⊢ ( 𝑢 ∼ 𝑤 ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑤 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑤 ) ∈ ℚ ) )
46 26 32 42 45 syl21anbrc ⊢ ( ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) → 𝑢 ∼ 𝑤 )
47 7 subidd ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → ( 𝑢 − 𝑢 ) = 0 )
48 0z ⊢ 0 ∈ ℤ
49 zq ⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
50 48 49 ax-mp ⊢ 0 ∈ ℚ
51 47 50 eqeltrdi ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → ( 𝑢 − 𝑢 ) ∈ ℚ )
52 51 adantr ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) → ( 𝑢 − 𝑢 ) ∈ ℚ )
53 52 pm4.71i ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑢 ) ∈ ℚ ) )
54 pm4.24 ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) ↔ ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) )
55 oveq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 − 𝑦 ) = ( 𝑢 − 𝑢 ) )
56 55 eleq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑢 − 𝑢 ) ∈ ℚ ) )
57 56 1 brab2a ⊢ ( 𝑢 ∼ 𝑢 ↔ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑢 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑢 − 𝑢 ) ∈ ℚ ) )
58 53 54 57 3bitr4i ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) ↔ 𝑢 ∼ 𝑢 )
59 2 23 46 58 iseri ⊢ ∼ Er ( 0 [,] 1 )