Metamath Proof Explorer

Theorem vitalilem2

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 vitalilem2 ( 𝜑 → ( ran 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∧ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) ) )

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 neeq1 ⊢ ( [ 𝑣 ] ∼ = 𝑧 → ( [ 𝑣 ] ∼ ≠ ∅ ↔ 𝑧 ≠ ∅ ) )
9 1 vitalilem1 ⊢ ∼ Er ( 0 [,] 1 )
10 erdm ⊢ ( ∼ Er ( 0 [,] 1 ) → dom ∼ = ( 0 [,] 1 ) )
11 9 10 ax-mp ⊢ dom ∼ = ( 0 [,] 1 )
12 11 eleq2i ⊢ ( 𝑣 ∈ dom ∼ ↔ 𝑣 ∈ ( 0 [,] 1 ) )
13 ecdmn0 ⊢ ( 𝑣 ∈ dom ∼ ↔ [ 𝑣 ] ∼ ≠ ∅ )
14 12 13 bitr3i ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) ↔ [ 𝑣 ] ∼ ≠ ∅ )
15 14 biimpi ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → [ 𝑣 ] ∼ ≠ ∅ )
16 2 8 15 ectocl ⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ≠ ∅ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ≠ ∅ )
18 sseq1 ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ ( 0 [,] 1 ) ↔ 𝑧 ⊆ ( 0 [,] 1 ) ) )
19 9 a1i ⊢ ( 𝑤 ∈ ( 0 [,] 1 ) → ∼ Er ( 0 [,] 1 ) )
20 19 ecss ⊢ ( 𝑤 ∈ ( 0 [,] 1 ) → [ 𝑤 ] ∼ ⊆ ( 0 [,] 1 ) )
21 2 18 20 ectocl ⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ⊆ ( 0 [,] 1 ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ⊆ ( 0 [,] 1 ) )
23 22 sseld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
24 17 23 embantd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
25 24 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
26 4 25 mpd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) )
27 ffnfv ⊢ ( 𝐹 : 𝑆 ⟶ ( 0 [,] 1 ) ↔ ( 𝐹 Fn 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] 1 ) ) )
28 3 26 27 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ( 0 [,] 1 ) )
29 28 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 [,] 1 ) )
30 5 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
31 f1ocnv ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → ◡ 𝐺 : ( ℚ ∩ ( - 1 [,] 1 ) ) –1-1-onto→ ℕ )
32 f1of ⊢ ( ◡ 𝐺 : ( ℚ ∩ ( - 1 [,] 1 ) ) –1-1-onto→ ℕ → ◡ 𝐺 : ( ℚ ∩ ( - 1 [,] 1 ) ) ⟶ ℕ )
33 30 31 32 3syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ◡ 𝐺 : ( ℚ ∩ ( - 1 [,] 1 ) ) ⟶ ℕ )
34 14 bilani ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ≠ ∅ )
35 neeq1 ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( 𝑧 ≠ ∅ ↔ [ 𝑣 ] ∼ ≠ ∅ ) )
36 fveq2 ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
37 id ⊢ ( 𝑧 = [ 𝑣 ] ∼ → 𝑧 = [ 𝑣 ] ∼ )
38 36 37 eleq12d ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) )
39 35 38 imbi12d ⊢ ( 𝑧 = [ 𝑣 ] ∼ → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( [ 𝑣 ] ∼ ≠ ∅ → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) ) )
40 4 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
41 ovex ⊢ ( 0 [,] 1 ) ∈ V
42 erex ⊢ ( ∼ Er ( 0 [,] 1 ) → ( ( 0 [,] 1 ) ∈ V → ∼ ∈ V ) )
43 9 41 42 mp2 ⊢ ∼ ∈ V
44 43 ecelqsi ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → [ 𝑣 ] ∼ ∈ ( ( 0 [,] 1 ) / ∼ ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ∈ ( ( 0 [,] 1 ) / ∼ ) )
46 45 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → [ 𝑣 ] ∼ ∈ 𝑆 )
47 39 40 46 rspcdva ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( [ 𝑣 ] ∼ ≠ ∅ → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ) )
48 34 47 mpd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ )
49 fvex ⊢ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ V
50 vex ⊢ 𝑣 ∈ V
51 49 50 elec ⊢ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ↔ 𝑣 ∼ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
52 oveq12 ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) → ( 𝑥 − 𝑦 ) = ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) )
53 52 eleq1d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) → ( ( 𝑥 − 𝑦 ) ∈ ℚ ↔ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℚ ) )
54 53 1 brab2a ⊢ ( 𝑣 ∼ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ↔ ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℚ ) )
55 51 54 bitri ⊢ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ [ 𝑣 ] ∼ ↔ ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℚ ) )
56 48 55 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝑣 ∈ ( 0 [,] 1 ) ∧ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ( 0 [,] 1 ) ) ∧ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℚ ) )
57 56 simprd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℚ )
58 elicc01 ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) ↔ ( 𝑣 ∈ ℝ ∧ 0 ≤ 𝑣 ∧ 𝑣 ≤ 1 ) )
59 58 bilani ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 ∈ ℝ ∧ 0 ≤ 𝑣 ∧ 𝑣 ≤ 1 ) )
60 59 simp1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ ℝ )
61 56 simpld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 ∈ ( 0 [,] 1 ) ∧ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ( 0 [,] 1 ) ) )
62 61 simprd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ( 0 [,] 1 ) )
63 elicc01 ⊢ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∧ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ≤ 1 ) )
64 62 63 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∧ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ≤ 1 ) )
65 64 simp1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ℝ )
66 60 65 resubcld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℝ )
67 65 60 resubcld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) ∈ ℝ )
68 1red ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℝ )
69 59 simp2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝑣 )
70 65 60 subge02d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 0 ≤ 𝑣 ↔ ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) ≤ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) )
71 69 70 mpbid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) ≤ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
72 64 simp3d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ≤ 1 )
73 67 65 68 71 72 letrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) ≤ 1 )
74 67 68 lenegd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) ≤ 1 ↔ - 1 ≤ - ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) ) )
75 73 74 mpbid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → - 1 ≤ - ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) )
76 65 recnd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ℂ )
77 60 recnd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ ℂ )
78 76 77 negsubdi2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → - ( ( 𝐹 ‘ [ 𝑣 ] ∼ ) − 𝑣 ) = ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) )
79 75 78 breqtrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → - 1 ≤ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) )
80 64 simp2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 0 ≤ ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
81 60 65 subge02d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 0 ≤ ( 𝐹 ‘ [ 𝑣 ] ∼ ) ↔ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ≤ 𝑣 ) )
82 80 81 mpbid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ≤ 𝑣 )
83 59 simp3d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ≤ 1 )
84 66 60 68 82 83 letrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ≤ 1 )
85 neg1rr ⊢ - 1 ∈ ℝ
86 1re ⊢ 1 ∈ ℝ
87 85 86 elicc2i ⊢ ( ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ( - 1 [,] 1 ) ↔ ( ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ℝ ∧ - 1 ≤ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∧ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ≤ 1 ) )
88 66 79 84 87 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ( - 1 [,] 1 ) )
89 57 88 elind ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ( ℚ ∩ ( - 1 [,] 1 ) ) )
90 33 89 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ∈ ℕ )
91 oveq1 ⊢ ( 𝑠 = 𝑣 → ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) = ( 𝑣 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) )
92 91 eleq1d ⊢ ( 𝑠 = 𝑣 → ( ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 ↔ ( 𝑣 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 ) )
93 f1ocnvfv2 ⊢ ( ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ∈ ( ℚ ∩ ( - 1 [,] 1 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) = ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) )
94 5 89 93 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) = ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) )
95 94 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) = ( 𝑣 − ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) )
96 77 76 nncand ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
97 95 96 eqtrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) = ( 𝐹 ‘ [ 𝑣 ] ∼ ) )
98 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑆 ∧ [ 𝑣 ] ∼ ∈ 𝑆 ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ran 𝐹 )
99 3 46 98 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ [ 𝑣 ] ∼ ) ∈ ran 𝐹 )
100 97 99 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑣 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 )
101 92 60 100 elrabd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 } )
102 fveq2 ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) )
103 102 oveq2d ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) → ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) = ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) )
104 103 eleq1d ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) → ( ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 ↔ ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 ) )
105 104 rabbidv ⊢ ( 𝑛 = ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 } )
106 reex ⊢ ℝ ∈ V
107 106 rabex ⊢ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 } ∈ V
108 105 6 107 fvmpt ⊢ ( ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ∈ ℕ → ( 𝑇 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 } )
109 90 108 syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑇 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) ∈ ran 𝐹 } )
110 101 109 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ ( 𝑇 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) )
111 fveq2 ⊢ ( 𝑚 = ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) → ( 𝑇 ‘ 𝑚 ) = ( 𝑇 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) )
112 111 eliuni ⊢ ( ( ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ∈ ℕ ∧ 𝑣 ∈ ( 𝑇 ‘ ( ◡ 𝐺 ‘ ( 𝑣 − ( 𝐹 ‘ [ 𝑣 ] ∼ ) ) ) ) ) → 𝑣 ∈ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )
113 90 110 112 syl2anc ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )
114 113 ex ⊢ ( 𝜑 → ( 𝑣 ∈ ( 0 [,] 1 ) → 𝑣 ∈ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
115 114 ssrdv ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )
116 eliun ⊢ ( 𝑥 ∈ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) )
117 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑚 ) )
118 117 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) = ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) )
119 118 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 ↔ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
120 119 rabbidv ⊢ ( 𝑛 = 𝑚 → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
121 106 rabex ⊢ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ∈ V
122 120 6 121 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( 𝑇 ‘ 𝑚 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
123 122 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑇 ‘ 𝑚 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
124 123 eleq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ↔ 𝑥 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ) )
125 124 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 𝑥 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
126 oveq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) = ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) )
127 126 eleq1d ⊢ ( 𝑠 = 𝑥 → ( ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ↔ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
128 127 elrab ⊢ ( 𝑥 ∈ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
129 125 128 sylib ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
130 129 simpld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 𝑥 ∈ ℝ )
131 85 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → - 1 ∈ ℝ )
132 iccssre ⊢ ( ( - 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( - 1 [,] 1 ) ⊆ ℝ )
133 85 86 132 mp2an ⊢ ( - 1 [,] 1 ) ⊆ ℝ
134 f1of ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
135 5 134 syl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
136 135 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ( ℚ ∩ ( - 1 [,] 1 ) ) )
137 136 elin2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ( - 1 [,] 1 ) )
138 133 137 sselid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ℝ )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℝ )
140 137 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ( - 1 [,] 1 ) )
141 85 86 elicc2i ⊢ ( ( 𝐺 ‘ 𝑚 ) ∈ ( - 1 [,] 1 ) ↔ ( ( 𝐺 ‘ 𝑚 ) ∈ ℝ ∧ - 1 ≤ ( 𝐺 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑚 ) ≤ 1 ) )
142 140 141 sylib ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( ( 𝐺 ‘ 𝑚 ) ∈ ℝ ∧ - 1 ≤ ( 𝐺 ‘ 𝑚 ) ∧ ( 𝐺 ‘ 𝑚 ) ≤ 1 ) )
143 142 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → - 1 ≤ ( 𝐺 ‘ 𝑚 ) )
144 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ran 𝐹 ⊆ ( 0 [,] 1 ) )
145 129 simprd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 )
146 144 145 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ( 0 [,] 1 ) )
147 elicc01 ⊢ ( ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∧ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ≤ 1 ) )
148 146 147 sylib ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ∧ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ≤ 1 ) )
149 148 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 0 ≤ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) )
150 130 139 subge0d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 0 ≤ ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ 𝑚 ) ≤ 𝑥 ) )
151 149 150 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑚 ) ≤ 𝑥 )
152 131 139 130 143 151 letrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → - 1 ≤ 𝑥 )
153 peano2re ⊢ ( ( 𝐺 ‘ 𝑚 ) ∈ ℝ → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ∈ ℝ )
154 139 153 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ∈ ℝ )
155 2re ⊢ 2 ∈ ℝ
156 155 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 2 ∈ ℝ )
157 148 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ≤ 1 )
158 1red ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 1 ∈ ℝ )
159 130 139 158 lesubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( ( 𝑥 − ( 𝐺 ‘ 𝑚 ) ) ≤ 1 ↔ 𝑥 ≤ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ) )
160 157 159 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 𝑥 ≤ ( ( 𝐺 ‘ 𝑚 ) + 1 ) )
161 142 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( 𝐺 ‘ 𝑚 ) ≤ 1 )
162 139 158 158 161 leadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ ( 1 + 1 ) )
163 df-2 ⊢ 2 = ( 1 + 1 )
164 162 163 breqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 2 )
165 130 154 156 160 164 letrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 𝑥 ≤ 2 )
166 85 155 elicc2i ⊢ ( 𝑥 ∈ ( - 1 [,] 2 ) ↔ ( 𝑥 ∈ ℝ ∧ - 1 ≤ 𝑥 ∧ 𝑥 ≤ 2 ) )
167 130 152 165 166 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) ) → 𝑥 ∈ ( - 1 [,] 2 ) )
168 167 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑇 ‘ 𝑚 ) → 𝑥 ∈ ( - 1 [,] 2 ) ) )
169 116 168 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) → 𝑥 ∈ ( - 1 [,] 2 ) ) )
170 169 ssrdv ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) )
171 29 115 170 3jca ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∧ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) ) )