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