Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vitalilem2 Structured version   Visualization version   GIF version

Theorem vitalilem2 23423
 Description: Lemma for vitali 23427. (Contributed by Mario Carneiro, 16-Jun-2014.)
Hypotheses
Ref Expression
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
Ref Expression
vitalilem2 (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ 𝑚 ∈ ℕ (𝑇𝑚) ∧ 𝑚 ∈ ℕ (𝑇𝑚) ⊆ (-1[,]2)))
Distinct variable groups:   𝑚,𝑛,𝑠,𝑥,𝑦,𝑧,𝐺   𝜑,𝑚,𝑛,𝑥,𝑧   𝑧,𝑆   𝑇,𝑚,𝑥   𝑚,𝐹,𝑛,𝑠,𝑥,𝑦,𝑧   ,𝑚,𝑛,𝑠,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑠)   𝑆(𝑥,𝑦,𝑚,𝑛,𝑠)   𝑇(𝑦,𝑧,𝑛,𝑠)

Proof of Theorem vitalilem2
Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vitali.3 . . . 4 (𝜑𝐹 Fn 𝑆)
2 vitali.4 . . . . 5 (𝜑 → ∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧))
3 vitali.2 . . . . . . . . 9 𝑆 = ((0[,]1) / )
4 neeq1 2885 . . . . . . . . 9 ([𝑣] = 𝑧 → ([𝑣] ≠ ∅ ↔ 𝑧 ≠ ∅))
5 vitali.1 . . . . . . . . . . . . . 14 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥𝑦) ∈ ℚ)}
65vitalilem1 23422 . . . . . . . . . . . . 13 Er (0[,]1)
7 erdm 7797 . . . . . . . . . . . . 13 ( Er (0[,]1) → dom = (0[,]1))
86, 7ax-mp 5 . . . . . . . . . . . 12 dom = (0[,]1)
98eleq2i 2722 . . . . . . . . . . 11 (𝑣 ∈ dom 𝑣 ∈ (0[,]1))
10 ecdmn0 7832 . . . . . . . . . . 11 (𝑣 ∈ dom ↔ [𝑣] ≠ ∅)
119, 10bitr3i 266 . . . . . . . . . 10 (𝑣 ∈ (0[,]1) ↔ [𝑣] ≠ ∅)
1211biimpi 206 . . . . . . . . 9 (𝑣 ∈ (0[,]1) → [𝑣] ≠ ∅)
133, 4, 12ectocl 7858 . . . . . . . 8 (𝑧𝑆𝑧 ≠ ∅)
1413adantl 481 . . . . . . 7 ((𝜑𝑧𝑆) → 𝑧 ≠ ∅)
15 sseq1 3659 . . . . . . . . . 10 ([𝑤] = 𝑧 → ([𝑤] ⊆ (0[,]1) ↔ 𝑧 ⊆ (0[,]1)))
166a1i 11 . . . . . . . . . . 11 (𝑤 ∈ (0[,]1) → Er (0[,]1))
1716ecss 7831 . . . . . . . . . 10 (𝑤 ∈ (0[,]1) → [𝑤] ⊆ (0[,]1))
183, 15, 17ectocl 7858 . . . . . . . . 9 (𝑧𝑆𝑧 ⊆ (0[,]1))
1918adantl 481 . . . . . . . 8 ((𝜑𝑧𝑆) → 𝑧 ⊆ (0[,]1))
2019sseld 3635 . . . . . . 7 ((𝜑𝑧𝑆) → ((𝐹𝑧) ∈ 𝑧 → (𝐹𝑧) ∈ (0[,]1)))
2114, 20embantd 59 . . . . . 6 ((𝜑𝑧𝑆) → ((𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧) → (𝐹𝑧) ∈ (0[,]1)))
2221ralimdva 2991 . . . . 5 (𝜑 → (∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧) → ∀𝑧𝑆 (𝐹𝑧) ∈ (0[,]1)))
232, 22mpd 15 . . . 4 (𝜑 → ∀𝑧𝑆 (𝐹𝑧) ∈ (0[,]1))
24 ffnfv 6428 . . . 4 (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧𝑆 (𝐹𝑧) ∈ (0[,]1)))
251, 23, 24sylanbrc 699 . . 3 (𝜑𝐹:𝑆⟶(0[,]1))
26 frn 6091 . . 3 (𝐹:𝑆⟶(0[,]1) → ran 𝐹 ⊆ (0[,]1))
2725, 26syl 17 . 2 (𝜑 → ran 𝐹 ⊆ (0[,]1))
28 vitali.5 . . . . . . . . 9 (𝜑𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
2928adantr 480 . . . . . . . 8 ((𝜑𝑣 ∈ (0[,]1)) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
30 f1ocnv 6187 . . . . . . . 8 (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:(ℚ ∩ (-1[,]1))–1-1-onto→ℕ)
31 f1of 6175 . . . . . . . 8 (𝐺:(ℚ ∩ (-1[,]1))–1-1-onto→ℕ → 𝐺:(ℚ ∩ (-1[,]1))⟶ℕ)
3229, 30, 313syl 18 . . . . . . 7 ((𝜑𝑣 ∈ (0[,]1)) → 𝐺:(ℚ ∩ (-1[,]1))⟶ℕ)
33 ovex 6718 . . . . . . . . . . . . . . 15 (0[,]1) ∈ V
34 erex 7811 . . . . . . . . . . . . . . 15 ( Er (0[,]1) → ((0[,]1) ∈ V → ∈ V))
356, 33, 34mp2 9 . . . . . . . . . . . . . 14 ∈ V
3635ecelqsi 7846 . . . . . . . . . . . . 13 (𝑣 ∈ (0[,]1) → [𝑣] ∈ ((0[,]1) / ))
3736adantl 481 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → [𝑣] ∈ ((0[,]1) / ))
3837, 3syl6eleqr 2741 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → [𝑣] 𝑆)
392adantr 480 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → ∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧))
40 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1))
4140, 11sylib 208 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → [𝑣] ≠ ∅)
42 neeq1 2885 . . . . . . . . . . . . 13 (𝑧 = [𝑣] → (𝑧 ≠ ∅ ↔ [𝑣] ≠ ∅))
43 fveq2 6229 . . . . . . . . . . . . . 14 (𝑧 = [𝑣] → (𝐹𝑧) = (𝐹‘[𝑣] ))
44 id 22 . . . . . . . . . . . . . 14 (𝑧 = [𝑣] 𝑧 = [𝑣] )
4543, 44eleq12d 2724 . . . . . . . . . . . . 13 (𝑧 = [𝑣] → ((𝐹𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ) ∈ [𝑣] ))
4642, 45imbi12d 333 . . . . . . . . . . . 12 (𝑧 = [𝑣] → ((𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧) ↔ ([𝑣] ≠ ∅ → (𝐹‘[𝑣] ) ∈ [𝑣] )))
4746rspcv 3336 . . . . . . . . . . 11 ([𝑣] 𝑆 → (∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧) → ([𝑣] ≠ ∅ → (𝐹‘[𝑣] ) ∈ [𝑣] )))
4838, 39, 41, 47syl3c 66 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ) ∈ [𝑣] )
49 fvex 6239 . . . . . . . . . . . 12 (𝐹‘[𝑣] ) ∈ V
50 vex 3234 . . . . . . . . . . . 12 𝑣 ∈ V
5149, 50elec 7829 . . . . . . . . . . 11 ((𝐹‘[𝑣] ) ∈ [𝑣] 𝑣 (𝐹‘[𝑣] ))
52 oveq12 6699 . . . . . . . . . . . . 13 ((𝑥 = 𝑣𝑦 = (𝐹‘[𝑣] )) → (𝑥𝑦) = (𝑣 − (𝐹‘[𝑣] )))
5352eleq1d 2715 . . . . . . . . . . . 12 ((𝑥 = 𝑣𝑦 = (𝐹‘[𝑣] )) → ((𝑥𝑦) ∈ ℚ ↔ (𝑣 − (𝐹‘[𝑣] )) ∈ ℚ))
5453, 5brab2a 5228 . . . . . . . . . . 11 (𝑣 (𝐹‘[𝑣] ) ↔ ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ) ∈ (0[,]1)) ∧ (𝑣 − (𝐹‘[𝑣] )) ∈ ℚ))
5551, 54bitri 264 . . . . . . . . . 10 ((𝐹‘[𝑣] ) ∈ [𝑣] ↔ ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ) ∈ (0[,]1)) ∧ (𝑣 − (𝐹‘[𝑣] )) ∈ ℚ))
5648, 55sylib 208 . . . . . . . . 9 ((𝜑𝑣 ∈ (0[,]1)) → ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ) ∈ (0[,]1)) ∧ (𝑣 − (𝐹‘[𝑣] )) ∈ ℚ))
5756simprd 478 . . . . . . . 8 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] )) ∈ ℚ)
58 0re 10078 . . . . . . . . . . . . 13 0 ∈ ℝ
59 1re 10077 . . . . . . . . . . . . 13 1 ∈ ℝ
6058, 59elicc2i 12277 . . . . . . . . . . . 12 (𝑣 ∈ (0[,]1) ↔ (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣𝑣 ≤ 1))
6140, 60sylib 208 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣𝑣 ≤ 1))
6261simp1d 1093 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 ∈ ℝ)
6356simpld 474 . . . . . . . . . . . . 13 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ) ∈ (0[,]1)))
6463simprd 478 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ) ∈ (0[,]1))
6558, 59elicc2i 12277 . . . . . . . . . . . 12 ((𝐹‘[𝑣] ) ∈ (0[,]1) ↔ ((𝐹‘[𝑣] ) ∈ ℝ ∧ 0 ≤ (𝐹‘[𝑣] ) ∧ (𝐹‘[𝑣] ) ≤ 1))
6664, 65sylib 208 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ) ∈ ℝ ∧ 0 ≤ (𝐹‘[𝑣] ) ∧ (𝐹‘[𝑣] ) ≤ 1))
6766simp1d 1093 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ) ∈ ℝ)
6862, 67resubcld 10496 . . . . . . . . 9 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] )) ∈ ℝ)
6967, 62resubcld 10496 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ) − 𝑣) ∈ ℝ)
70 1red 10093 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → 1 ∈ ℝ)
7161simp2d 1094 . . . . . . . . . . . . 13 ((𝜑𝑣 ∈ (0[,]1)) → 0 ≤ 𝑣)
7267, 62subge02d 10657 . . . . . . . . . . . . 13 ((𝜑𝑣 ∈ (0[,]1)) → (0 ≤ 𝑣 ↔ ((𝐹‘[𝑣] ) − 𝑣) ≤ (𝐹‘[𝑣] )))
7371, 72mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ) − 𝑣) ≤ (𝐹‘[𝑣] ))
7466simp3d 1095 . . . . . . . . . . . 12 ((𝜑𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ) ≤ 1)
7569, 67, 70, 73, 74letrd 10232 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ) − 𝑣) ≤ 1)
7669, 70lenegd 10644 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → (((𝐹‘[𝑣] ) − 𝑣) ≤ 1 ↔ -1 ≤ -((𝐹‘[𝑣] ) − 𝑣)))
7775, 76mpbid 222 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → -1 ≤ -((𝐹‘[𝑣] ) − 𝑣))
7867recnd 10106 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ) ∈ ℂ)
7962recnd 10106 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 ∈ ℂ)
8078, 79negsubdi2d 10446 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → -((𝐹‘[𝑣] ) − 𝑣) = (𝑣 − (𝐹‘[𝑣] )))
8177, 80breqtrd 4711 . . . . . . . . 9 ((𝜑𝑣 ∈ (0[,]1)) → -1 ≤ (𝑣 − (𝐹‘[𝑣] )))
8266simp2d 1094 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → 0 ≤ (𝐹‘[𝑣] ))
8362, 67subge02d 10657 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → (0 ≤ (𝐹‘[𝑣] ) ↔ (𝑣 − (𝐹‘[𝑣] )) ≤ 𝑣))
8482, 83mpbid 222 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] )) ≤ 𝑣)
8561simp3d 1095 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 ≤ 1)
8668, 62, 70, 84, 85letrd 10232 . . . . . . . . 9 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] )) ≤ 1)
87 neg1rr 11163 . . . . . . . . . 10 -1 ∈ ℝ
8887, 59elicc2i 12277 . . . . . . . . 9 ((𝑣 − (𝐹‘[𝑣] )) ∈ (-1[,]1) ↔ ((𝑣 − (𝐹‘[𝑣] )) ∈ ℝ ∧ -1 ≤ (𝑣 − (𝐹‘[𝑣] )) ∧ (𝑣 − (𝐹‘[𝑣] )) ≤ 1))
8968, 81, 86, 88syl3anbrc 1265 . . . . . . . 8 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] )) ∈ (-1[,]1))
9057, 89elind 3831 . . . . . . 7 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] )) ∈ (ℚ ∩ (-1[,]1)))
9132, 90ffvelrnd 6400 . . . . . 6 ((𝜑𝑣 ∈ (0[,]1)) → (𝐺‘(𝑣 − (𝐹‘[𝑣] ))) ∈ ℕ)
92 f1ocnvfv2 6573 . . . . . . . . . . . 12 ((𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ (𝑣 − (𝐹‘[𝑣] )) ∈ (ℚ ∩ (-1[,]1))) → (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))) = (𝑣 − (𝐹‘[𝑣] )))
9329, 90, 92syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑣 ∈ (0[,]1)) → (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))) = (𝑣 − (𝐹‘[𝑣] )))
9493oveq2d 6706 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) = (𝑣 − (𝑣 − (𝐹‘[𝑣] ))))
9579, 78nncand 10435 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝑣 − (𝐹‘[𝑣] ))) = (𝐹‘[𝑣] ))
9694, 95eqtrd 2685 . . . . . . . . 9 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) = (𝐹‘[𝑣] ))
971adantr 480 . . . . . . . . . 10 ((𝜑𝑣 ∈ (0[,]1)) → 𝐹 Fn 𝑆)
98 fnfvelrn 6396 . . . . . . . . . 10 ((𝐹 Fn 𝑆 ∧ [𝑣] 𝑆) → (𝐹‘[𝑣] ) ∈ ran 𝐹)
9997, 38, 98syl2anc 694 . . . . . . . . 9 ((𝜑𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ) ∈ ran 𝐹)
10096, 99eqeltrd 2730 . . . . . . . 8 ((𝜑𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹)
101 oveq1 6697 . . . . . . . . . 10 (𝑠 = 𝑣 → (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) = (𝑣 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))))
102101eleq1d 2715 . . . . . . . . 9 (𝑠 = 𝑣 → ((𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹 ↔ (𝑣 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹))
103102elrab 3396 . . . . . . . 8 (𝑣 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹} ↔ (𝑣 ∈ ℝ ∧ (𝑣 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹))
10462, 100, 103sylanbrc 699 . . . . . . 7 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹})
105 fveq2 6229 . . . . . . . . . . . 12 (𝑛 = (𝐺‘(𝑣 − (𝐹‘[𝑣] ))) → (𝐺𝑛) = (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))))
106105oveq2d 6706 . . . . . . . . . . 11 (𝑛 = (𝐺‘(𝑣 − (𝐹‘[𝑣] ))) → (𝑠 − (𝐺𝑛)) = (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))))
107106eleq1d 2715 . . . . . . . . . 10 (𝑛 = (𝐺‘(𝑣 − (𝐹‘[𝑣] ))) → ((𝑠 − (𝐺𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹))
108107rabbidv 3220 . . . . . . . . 9 (𝑛 = (𝐺‘(𝑣 − (𝐹‘[𝑣] ))) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹})
109 vitali.6 . . . . . . . . 9 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹})
110 reex 10065 . . . . . . . . . 10 ℝ ∈ V
111110rabex 4845 . . . . . . . . 9 {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹} ∈ V
112108, 109, 111fvmpt 6321 . . . . . . . 8 ((𝐺‘(𝑣 − (𝐹‘[𝑣] ))) ∈ ℕ → (𝑇‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹})
11391, 112syl 17 . . . . . . 7 ((𝜑𝑣 ∈ (0[,]1)) → (𝑇‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) ∈ ran 𝐹})
114104, 113eleqtrrd 2733 . . . . . 6 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 ∈ (𝑇‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))))
11591, 114jca 553 . . . . 5 ((𝜑𝑣 ∈ (0[,]1)) → ((𝐺‘(𝑣 − (𝐹‘[𝑣] ))) ∈ ℕ ∧ 𝑣 ∈ (𝑇‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))))
116 fveq2 6229 . . . . . 6 (𝑚 = (𝐺‘(𝑣 − (𝐹‘[𝑣] ))) → (𝑇𝑚) = (𝑇‘(𝐺‘(𝑣 − (𝐹‘[𝑣] )))))
117116eliuni 4558 . . . . 5 (((𝐺‘(𝑣 − (𝐹‘[𝑣] ))) ∈ ℕ ∧ 𝑣 ∈ (𝑇‘(𝐺‘(𝑣 − (𝐹‘[𝑣] ))))) → 𝑣 𝑚 ∈ ℕ (𝑇𝑚))
118115, 117syl 17 . . . 4 ((𝜑𝑣 ∈ (0[,]1)) → 𝑣 𝑚 ∈ ℕ (𝑇𝑚))
119118ex 449 . . 3 (𝜑 → (𝑣 ∈ (0[,]1) → 𝑣 𝑚 ∈ ℕ (𝑇𝑚)))
120119ssrdv 3642 . 2 (𝜑 → (0[,]1) ⊆ 𝑚 ∈ ℕ (𝑇𝑚))
121 eliun 4556 . . . 4 (𝑥 𝑚 ∈ ℕ (𝑇𝑚) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑇𝑚))
122 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (𝐺𝑛) = (𝐺𝑚))
123122oveq2d 6706 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝑠 − (𝐺𝑛)) = (𝑠 − (𝐺𝑚)))
124123eleq1d 2715 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((𝑠 − (𝐺𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹))
125124rabbidv 3220 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹})
126110rabex 4845 . . . . . . . . . . . . 13 {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹} ∈ V
127125, 109, 126fvmpt 6321 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → (𝑇𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹})
128127adantl 481 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝑇𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹})
129128eleq2d 2716 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ (𝑇𝑚) ↔ 𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹}))
130129biimpa 500 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹})
131 oveq1 6697 . . . . . . . . . . 11 (𝑠 = 𝑥 → (𝑠 − (𝐺𝑚)) = (𝑥 − (𝐺𝑚)))
132131eleq1d 2715 . . . . . . . . . 10 (𝑠 = 𝑥 → ((𝑠 − (𝐺𝑚)) ∈ ran 𝐹 ↔ (𝑥 − (𝐺𝑚)) ∈ ran 𝐹))
133132elrab 3396 . . . . . . . . 9 (𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑚)) ∈ ran 𝐹} ↔ (𝑥 ∈ ℝ ∧ (𝑥 − (𝐺𝑚)) ∈ ran 𝐹))
134130, 133sylib 208 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝑥 ∈ ℝ ∧ (𝑥 − (𝐺𝑚)) ∈ ran 𝐹))
135134simpld 474 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 𝑥 ∈ ℝ)
13687a1i 11 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → -1 ∈ ℝ)
137 iccssre 12293 . . . . . . . . . . 11 ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
13887, 59, 137mp2an 708 . . . . . . . . . 10 (-1[,]1) ⊆ ℝ
139 inss2 3867 . . . . . . . . . . 11 (ℚ ∩ (-1[,]1)) ⊆ (-1[,]1)
140 f1of 6175 . . . . . . . . . . . . 13 (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
14128, 140syl 17 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
142141ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) ∈ (ℚ ∩ (-1[,]1)))
143139, 142sseldi 3634 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) ∈ (-1[,]1))
144138, 143sseldi 3634 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) ∈ ℝ)
145144adantr 480 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝐺𝑚) ∈ ℝ)
146143adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝐺𝑚) ∈ (-1[,]1))
14787, 59elicc2i 12277 . . . . . . . . . 10 ((𝐺𝑚) ∈ (-1[,]1) ↔ ((𝐺𝑚) ∈ ℝ ∧ -1 ≤ (𝐺𝑚) ∧ (𝐺𝑚) ≤ 1))
148146, 147sylib 208 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ((𝐺𝑚) ∈ ℝ ∧ -1 ≤ (𝐺𝑚) ∧ (𝐺𝑚) ≤ 1))
149148simp2d 1094 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → -1 ≤ (𝐺𝑚))
15027ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ran 𝐹 ⊆ (0[,]1))
151134simprd 478 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝑥 − (𝐺𝑚)) ∈ ran 𝐹)
152150, 151sseldd 3637 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝑥 − (𝐺𝑚)) ∈ (0[,]1))
15358, 59elicc2i 12277 . . . . . . . . . . 11 ((𝑥 − (𝐺𝑚)) ∈ (0[,]1) ↔ ((𝑥 − (𝐺𝑚)) ∈ ℝ ∧ 0 ≤ (𝑥 − (𝐺𝑚)) ∧ (𝑥 − (𝐺𝑚)) ≤ 1))
154152, 153sylib 208 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ((𝑥 − (𝐺𝑚)) ∈ ℝ ∧ 0 ≤ (𝑥 − (𝐺𝑚)) ∧ (𝑥 − (𝐺𝑚)) ≤ 1))
155154simp2d 1094 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 0 ≤ (𝑥 − (𝐺𝑚)))
156135, 145subge0d 10655 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (0 ≤ (𝑥 − (𝐺𝑚)) ↔ (𝐺𝑚) ≤ 𝑥))
157155, 156mpbid 222 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝐺𝑚) ≤ 𝑥)
158136, 145, 135, 149, 157letrd 10232 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → -1 ≤ 𝑥)
159 peano2re 10247 . . . . . . . . 9 ((𝐺𝑚) ∈ ℝ → ((𝐺𝑚) + 1) ∈ ℝ)
160145, 159syl 17 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ((𝐺𝑚) + 1) ∈ ℝ)
161 2re 11128 . . . . . . . . 9 2 ∈ ℝ
162161a1i 11 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 2 ∈ ℝ)
163154simp3d 1095 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝑥 − (𝐺𝑚)) ≤ 1)
164 1red 10093 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 1 ∈ ℝ)
165135, 145, 164lesubadd2d 10664 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ((𝑥 − (𝐺𝑚)) ≤ 1 ↔ 𝑥 ≤ ((𝐺𝑚) + 1)))
166163, 165mpbid 222 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 𝑥 ≤ ((𝐺𝑚) + 1))
167148simp3d 1095 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → (𝐺𝑚) ≤ 1)
168145, 164, 164, 167leadd1dd 10679 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ((𝐺𝑚) + 1) ≤ (1 + 1))
169 df-2 11117 . . . . . . . . 9 2 = (1 + 1)
170168, 169syl6breqr 4727 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → ((𝐺𝑚) + 1) ≤ 2)
171135, 160, 162, 166, 170letrd 10232 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 𝑥 ≤ 2)
17287, 161elicc2i 12277 . . . . . . 7 (𝑥 ∈ (-1[,]2) ↔ (𝑥 ∈ ℝ ∧ -1 ≤ 𝑥𝑥 ≤ 2))
173135, 158, 171, 172syl3anbrc 1265 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇𝑚)) → 𝑥 ∈ (-1[,]2))
174173ex 449 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝑥 ∈ (𝑇𝑚) → 𝑥 ∈ (-1[,]2)))
175174rexlimdva 3060 . . . 4 (𝜑 → (∃𝑚 ∈ ℕ 𝑥 ∈ (𝑇𝑚) → 𝑥 ∈ (-1[,]2)))
176121, 175syl5bi 232 . . 3 (𝜑 → (𝑥 𝑚 ∈ ℕ (𝑇𝑚) → 𝑥 ∈ (-1[,]2)))
177176ssrdv 3642 . 2 (𝜑 𝑚 ∈ ℕ (𝑇𝑚) ⊆ (-1[,]2))
17827, 120, 1773jca 1261 1 (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ 𝑚 ∈ ℕ (𝑇𝑚) ∧ 𝑚 ∈ ℕ (𝑇𝑚) ⊆ (-1[,]2)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191  ∪ ciun 4552   class class class wbr 4685  {copab 4745   ↦ cmpt 4762  ◡ccnv 5142  dom cdm 5143  ran crn 5144   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   Er wer 7784  [cec 7785   / cqs 7786  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   ≤ cle 10113   − cmin 10304  -cneg 10305  ℕcn 11058  2c2 11108  ℚcq 11826  [,]cicc 12216  volcvol 23278 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-ec 7789  df-qs 7793  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-q 11827  df-icc 12220 This theorem is referenced by:  vitalilem3  23424  vitalilem4  23425  vitalilem5  23426
 Copyright terms: Public domain W3C validator