Metamath Proof Explorer

Theorem vitalilem5

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
vitali.2 ⊢ 𝑆 = ( ( 0 [,] 1 ) / ∼ )
vitali.3 ⊢ ( 𝜑 → 𝐹 Fn 𝑆 )
vitali.4 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
vitali.5 ⊢ ( 𝜑 → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
vitali.6 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } )
vitali.7 ⊢ ( 𝜑 → ¬ ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) )
Assertion vitalilem5 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 vitali.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
2 vitali.2 ⊢ 𝑆 = ( ( 0 [,] 1 ) / ∼ )
3 vitali.3 ⊢ ( 𝜑 → 𝐹 Fn 𝑆 )
4 vitali.4 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
5 vitali.5 ⊢ ( 𝜑 → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
6 vitali.6 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } )
7 vitali.7 ⊢ ( 𝜑 → ¬ ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) )
8 0lt1 ⊢ 0 < 1
9 0re ⊢ 0 ∈ ℝ
10 1re ⊢ 1 ∈ ℝ
11 0le1 ⊢ 0 ≤ 1
12 ovolicc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1 ) → ( vol* ‘ ( 0 [,] 1 ) ) = ( 1 − 0 ) )
13 9 10 11 12 mp3an ⊢ ( vol* ‘ ( 0 [,] 1 ) ) = ( 1 − 0 )
14 1m0e1 ⊢ ( 1 − 0 ) = 1
15 13 14 eqtri ⊢ ( vol* ‘ ( 0 [,] 1 ) ) = 1
16 8 15 breqtrri ⊢ 0 < ( vol* ‘ ( 0 [,] 1 ) )
17 15 10 eqeltri ⊢ ( vol* ‘ ( 0 [,] 1 ) ) ∈ ℝ
18 9 17 ltnlei ⊢ ( 0 < ( vol* ‘ ( 0 [,] 1 ) ) ↔ ¬ ( vol* ‘ ( 0 [,] 1 ) ) ≤ 0 )
19 16 18 mpbi ⊢ ¬ ( vol* ‘ ( 0 [,] 1 ) ) ≤ 0
20 1 2 3 4 5 6 7 vitalilem2 ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∧ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) ) )
21 20 simp2d ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )
22 1 vitalilem1 ⊢ ∼ Er ( 0 [,] 1 )
23 erdm ⊢ ( ∼ Er ( 0 [,] 1 ) → dom ∼ = ( 0 [,] 1 ) )
24 22 23 ax-mp ⊢ dom ∼ = ( 0 [,] 1 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
26 25 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ ( ( 0 [,] 1 ) / ∼ ) )
27 elqsn0 ⊢ ( ( dom ∼ = ( 0 [,] 1 ) ∧ 𝑧 ∈ ( ( 0 [,] 1 ) / ∼ ) ) → 𝑧 ≠ ∅ )
28 24 26 27 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ≠ ∅ )
29 22 a1i ⊢ ( 𝜑 → ∼ Er ( 0 [,] 1 ) )
30 29 qsss ⊢ ( 𝜑 → ( ( 0 [,] 1 ) / ∼ ) ⊆ 𝒫 ( 0 [,] 1 ) )
31 2 30 eqsstrid ⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 ( 0 [,] 1 ) )
32 31 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝒫 ( 0 [,] 1 ) )
33 32 elpwid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ⊆ ( 0 [,] 1 ) )
34 33 sseld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
35 28 34 embantd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
36 35 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
37 4 36 mpd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) )
38 ffnfv ⊢ ( 𝐹 : 𝑆 ⟶ ( 0 [,] 1 ) ↔ ( 𝐹 Fn 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
39 3 37 38 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ( 0 [,] 1 ) )
40 39 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 [,] 1 ) )
41 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
42 40 41 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
43 reex ⊢ ℝ ∈ V
44 43 elpw2 ⊢ ( ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ )
45 42 44 sylibr ⊢ ( 𝜑 → ran 𝐹 ∈ 𝒫 ℝ )
46 45 anim1i ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ∈ dom vol ) → ( ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol ) )
47 eldif ⊢ ( ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) ↔ ( ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol ) )
48 46 47 sylibr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ∈ dom vol ) → ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) )
49 48 ex ⊢ ( 𝜑 → ( ¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) ) )
50 7 49 mt3d ⊢ ( 𝜑 → ran 𝐹 ∈ dom vol )
51 f1of ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
52 5 51 syl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
53 inss1 ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℚ
54 qssre ⊢ ℚ ⊆ ℝ
55 53 54 sstri ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℝ
56 fss ⊢ ( ( 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℝ ) → 𝐺 : ℕ ⟶ ℝ )
57 52 55 56 sylancl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ℝ )
58 57 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
59 shftmbl ⊢ ( ( ran 𝐹 ∈ dom vol ∧ ( 𝐺 ‘ 𝑛 ) ∈ ℝ ) → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } ∈ dom vol )
60 50 58 59 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } ∈ dom vol )
61 60 6 fmptd ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ dom vol )
62 61 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
63 62 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
64 iunmbl ⊢ ( ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
65 63 64 syl ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
66 mblss ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ )
67 65 66 syl ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ )
68 ovolss ⊢ ( ( ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∧ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ ) → ( vol* ‘ ( 0 [,] 1 ) ) ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
69 21 67 68 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 0 [,] 1 ) ) ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
70 eqid ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) )
71 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) )
72 mblss ⊢ ( ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ( 𝑇 ‘ 𝑚 ) ⊆ ℝ )
73 62 72 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑇 ‘ 𝑚 ) ⊆ ℝ )
74 1 2 3 4 5 6 7 vitalilem4 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = 0 )
75 74 9 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ )
76 74 mpteq2dva ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ 0 ) )
77 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑚 ∈ ℕ ↦ 0 )
78 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
79 78 xpeq1i ⊢ ( ℕ × { 0 } ) = ( ( ℤ≥ ‘ 1 ) × { 0 } )
80 77 79 eqtr3i ⊢ ( 𝑚 ∈ ℕ ↦ 0 ) = ( ( ℤ≥ ‘ 1 ) × { 0 } )
81 76 80 eqtrdi ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) = ( ( ℤ≥ ‘ 1 ) × { 0 } ) )
82 81 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) = seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) )
83 1z ⊢ 1 ∈ ℤ
84 serclim0 ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0 )
85 83 84 ax-mp ⊢ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0
86 82 85 eqbrtrdi ⊢ ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ⇝ 0 )
87 seqex ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ∈ V
88 c0ex ⊢ 0 ∈ V
89 87 88 breldm ⊢ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ⇝ 0 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ∈ dom ⇝ )
90 86 89 syl ⊢ ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ∈ dom ⇝ )
91 70 71 73 75 90 ovoliun2 ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ Σ 𝑚 ∈ ℕ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) )
92 74 sumeq2dv ⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = Σ 𝑚 ∈ ℕ 0 )
93 78 eqimssi ⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
94 93 orci ⊢ ( ℕ ⊆ ( ℤ≥ ‘ 1 ) ∨ ℕ ∈ Fin )
95 sumz ⊢ ( ( ℕ ⊆ ( ℤ≥ ‘ 1 ) ∨ ℕ ∈ Fin ) → Σ 𝑚 ∈ ℕ 0 = 0 )
96 94 95 ax-mp ⊢ Σ 𝑚 ∈ ℕ 0 = 0
97 92 96 eqtrdi ⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = 0 )
98 91 97 breqtrd ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ 0 )
99 ovolge0 ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ → 0 ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
100 67 99 syl ⊢ ( 𝜑 → 0 ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
101 ovolcl ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* )
102 67 101 syl ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* )
103 0xr ⊢ 0 ∈ ℝ*
104 xrletri3 ⊢ ( ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = 0 ↔ ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ 0 ∧ 0 ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ) ) )
105 102 103 104 sylancl ⊢ ( 𝜑 → ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = 0 ↔ ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ 0 ∧ 0 ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ) ) )
106 98 100 105 mpbir2and ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = 0 )
107 69 106 breqtrd ⊢ ( 𝜑 → ( vol* ‘ ( 0 [,] 1 ) ) ≤ 0 )
108 19 107 mto ⊢ ¬ 𝜑