Step | Hyp | Ref
| Expression |
1 | | vitali.3 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝑆) |
2 | | vitali.4 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
3 | | vitali.2 |
. . . . . . . . 9
⊢ 𝑆 = ((0[,]1) / ∼
) |
4 | | neeq1 2856 |
. . . . . . . . 9
⊢ ([𝑣] ∼ = 𝑧 → ([𝑣] ∼ ≠ ∅ ↔
𝑧 ≠
∅)) |
5 | | vitali.1 |
. . . . . . . . . . . . . 14
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
6 | 5 | vitalilem1 23376 |
. . . . . . . . . . . . 13
⊢ ∼ Er
(0[,]1) |
7 | | erdm 7752 |
. . . . . . . . . . . . 13
⊢ ( ∼ Er
(0[,]1) → dom ∼ =
(0[,]1)) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom ∼ =
(0[,]1) |
9 | 8 | eleq2i 2693 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈
(0[,]1)) |
10 | | ecdmn0 7789 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠
∅) |
11 | 9, 10 | bitr3i 266 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠
∅) |
12 | 11 | biimpi 206 |
. . . . . . . . 9
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ≠
∅) |
13 | 3, 4, 12 | ectocl 7815 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → 𝑧 ≠ ∅) |
14 | 13 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ≠ ∅) |
15 | | sseq1 3626 |
. . . . . . . . . 10
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ (0[,]1)
↔ 𝑧 ⊆
(0[,]1))) |
16 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (0[,]1) → ∼ Er
(0[,]1)) |
17 | 16 | ecss 7788 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (0[,]1) → [𝑤] ∼ ⊆
(0[,]1)) |
18 | 3, 15, 17 | ectocl 7815 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑆 → 𝑧 ⊆ (0[,]1)) |
19 | 18 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ⊆ (0[,]1)) |
20 | 19 | sseld 3602 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) ∈ 𝑧 → (𝐹‘𝑧) ∈ (0[,]1))) |
21 | 14, 20 | embantd 59 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → (𝐹‘𝑧) ∈ (0[,]1))) |
22 | 21 | ralimdva 2962 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
23 | 2, 22 | mpd 15 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1)) |
24 | | ffnfv 6388 |
. . . 4
⊢ (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
25 | 1, 23, 24 | sylanbrc 698 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶(0[,]1)) |
26 | | frn 6053 |
. . 3
⊢ (𝐹:𝑆⟶(0[,]1) → ran 𝐹 ⊆ (0[,]1)) |
27 | 25, 26 | syl 17 |
. 2
⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1)) |
28 | | vitali.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
29 | 28 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
30 | | f1ocnv 6149 |
. . . . . . . 8
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → ◡𝐺:(ℚ ∩ (-1[,]1))–1-1-onto→ℕ) |
31 | | f1of 6137 |
. . . . . . . 8
⊢ (◡𝐺:(ℚ ∩ (-1[,]1))–1-1-onto→ℕ → ◡𝐺:(ℚ ∩
(-1[,]1))⟶ℕ) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ◡𝐺:(ℚ ∩
(-1[,]1))⟶ℕ) |
33 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (0[,]1)
∈ V |
34 | | erex 7766 |
. . . . . . . . . . . . . . 15
⊢ ( ∼ Er
(0[,]1) → ((0[,]1) ∈ V → ∼ ∈
V)) |
35 | 6, 33, 34 | mp2 9 |
. . . . . . . . . . . . . 14
⊢ ∼ ∈
V |
36 | 35 | ecelqsi 7803 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1)
/ ∼ )) |
37 | 36 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ ((0[,]1)
/ ∼ )) |
38 | 37, 3 | syl6eleqr 2712 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆) |
39 | 2 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
40 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1)) |
41 | 40, 11 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠
∅) |
42 | | neeq1 2856 |
. . . . . . . . . . . . 13
⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠
∅)) |
43 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ )) |
44 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ ) |
45 | 43, 44 | eleq12d 2695 |
. . . . . . . . . . . . 13
⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )) |
46 | 42, 45 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
47 | 46 | rspcv 3305 |
. . . . . . . . . . 11
⊢ ([𝑣] ∼ ∈ 𝑆 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
48 | 38, 39, 41, 47 | syl3c 66 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ) |
49 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ (𝐹‘[𝑣] ∼ ) ∈
V |
50 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
51 | 49, 50 | elec 7786 |
. . . . . . . . . . 11
⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ )) |
52 | | oveq12 6659 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = (𝐹‘[𝑣] ∼ )) → (𝑥 − 𝑦) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
53 | 52 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = (𝐹‘[𝑣] ∼ )) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
54 | 53, 5 | brab2a 5194 |
. . . . . . . . . . 11
⊢ (𝑣 ∼ (𝐹‘[𝑣] ∼ ) ↔ ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈ (0[,]1))
∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
55 | 51, 54 | bitri 264 |
. . . . . . . . . 10
⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈ (0[,]1))
∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
56 | 48, 55 | sylib 208 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈ (0[,]1))
∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
57 | 56 | simprd 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ) |
58 | | 0re 10040 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
59 | | 1re 10039 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
60 | 58, 59 | elicc2i 12239 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (0[,]1) ↔ (𝑣 ∈ ℝ ∧ 0 ≤
𝑣 ∧ 𝑣 ≤ 1)) |
61 | 40, 60 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣 ∧ 𝑣 ≤ 1)) |
62 | 61 | simp1d 1073 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ ℝ) |
63 | 56 | simpld 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈
(0[,]1))) |
64 | 63 | simprd 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈
(0[,]1)) |
65 | 58, 59 | elicc2i 12239 |
. . . . . . . . . . . 12
⊢ ((𝐹‘[𝑣] ∼ ) ∈ (0[,]1)
↔ ((𝐹‘[𝑣] ∼ ) ∈ ℝ
∧ 0 ≤ (𝐹‘[𝑣] ∼ ) ∧ (𝐹‘[𝑣] ∼ ) ≤
1)) |
66 | 64, 65 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) ∈ ℝ
∧ 0 ≤ (𝐹‘[𝑣] ∼ ) ∧ (𝐹‘[𝑣] ∼ ) ≤
1)) |
67 | 66 | simp1d 1073 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈
ℝ) |
68 | 62, 67 | resubcld 10458 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℝ) |
69 | 67, 62 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) − 𝑣) ∈
ℝ) |
70 | | 1red 10055 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 1 ∈
ℝ) |
71 | 61 | simp2d 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 0 ≤ 𝑣) |
72 | 67, 62 | subge02d 10619 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (0 ≤ 𝑣 ↔ ((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ (𝐹‘[𝑣] ∼
))) |
73 | 71, 72 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ (𝐹‘[𝑣] ∼ )) |
74 | 66 | simp3d 1075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ≤
1) |
75 | 69, 67, 70, 73, 74 | letrd 10194 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ 1) |
76 | 69, 70 | lenegd 10606 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ 1 ↔ -1 ≤ -((𝐹‘[𝑣] ∼ ) − 𝑣))) |
77 | 75, 76 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → -1 ≤ -((𝐹‘[𝑣] ∼ ) − 𝑣)) |
78 | 67 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈
ℂ) |
79 | 62 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ ℂ) |
80 | 78, 79 | negsubdi2d 10408 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → -((𝐹‘[𝑣] ∼ ) − 𝑣) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
81 | 77, 80 | breqtrd 4679 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → -1 ≤ (𝑣 − (𝐹‘[𝑣] ∼
))) |
82 | 66 | simp2d 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 0 ≤ (𝐹‘[𝑣] ∼ )) |
83 | 62, 67 | subge02d 10619 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (0 ≤ (𝐹‘[𝑣] ∼ ) ↔ (𝑣 − (𝐹‘[𝑣] ∼ )) ≤ 𝑣)) |
84 | 82, 83 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ≤ 𝑣) |
85 | 61 | simp3d 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ≤ 1) |
86 | 68, 62, 70, 84, 85 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ≤
1) |
87 | | neg1rr 11125 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
88 | 87, 59 | elicc2i 12239 |
. . . . . . . . 9
⊢ ((𝑣 − (𝐹‘[𝑣] ∼ )) ∈ (-1[,]1)
↔ ((𝑣 − (𝐹‘[𝑣] ∼ )) ∈ ℝ
∧ -1 ≤ (𝑣 −
(𝐹‘[𝑣] ∼ )) ∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ≤
1)) |
89 | 68, 81, 86, 88 | syl3anbrc 1246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
(-1[,]1)) |
90 | 57, 89 | elind 3798 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈ (ℚ
∩ (-1[,]1))) |
91 | 32, 90 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈
ℕ) |
92 | | f1ocnvfv2 6533 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈ (ℚ
∩ (-1[,]1))) → (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
93 | 29, 90, 92 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
94 | 93 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) = (𝑣 − (𝑣 − (𝐹‘[𝑣] ∼
)))) |
95 | 79, 78 | nncand 10397 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝑣 − (𝐹‘[𝑣] ∼ ))) = (𝐹‘[𝑣] ∼ )) |
96 | 94, 95 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) = (𝐹‘[𝑣] ∼ )) |
97 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝐹 Fn 𝑆) |
98 | | fnfvelrn 6356 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝑆 ∧ [𝑣] ∼ ∈ 𝑆) → (𝐹‘[𝑣] ∼ ) ∈ ran 𝐹) |
99 | 97, 38, 98 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ ran 𝐹) |
100 | 96, 99 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹) |
101 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑣 → (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) = (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
)))))) |
102 | 101 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑠 = 𝑣 → ((𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹 ↔ (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹)) |
103 | 102 | elrab 3363 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹} ↔ (𝑣 ∈ ℝ ∧ (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹)) |
104 | 62, 100, 103 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
105 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → (𝐺‘𝑛) = (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
))))) |
106 | 105 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
)))))) |
107 | 106 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹)) |
108 | 107 | rabbidv 3189 |
. . . . . . . . 9
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
109 | | vitali.6 |
. . . . . . . . 9
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹}) |
110 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
111 | 110 | rabex 4813 |
. . . . . . . . 9
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹} ∈
V |
112 | 108, 109,
111 | fvmpt 6282 |
. . . . . . . 8
⊢ ((◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈ ℕ
→ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
113 | 91, 112 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
114 | 104, 113 | eleqtrrd 2704 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
))))) |
115 | 91, 114 | jca 554 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈ ℕ
∧ 𝑣 ∈ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
)))))) |
116 | | fveq2 6191 |
. . . . . 6
⊢ (𝑚 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → (𝑇‘𝑚) = (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
))))) |
117 | 116 | eliuni 4526 |
. . . . 5
⊢ (((◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈ ℕ
∧ 𝑣 ∈ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) → 𝑣 ∈ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) |
118 | 115, 117 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ ∪
𝑚 ∈ ℕ (𝑇‘𝑚)) |
119 | 118 | ex 450 |
. . 3
⊢ (𝜑 → (𝑣 ∈ (0[,]1) → 𝑣 ∈ ∪
𝑚 ∈ ℕ (𝑇‘𝑚))) |
120 | 119 | ssrdv 3609 |
. 2
⊢ (𝜑 → (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) |
121 | | eliun 4524 |
. . . 4
⊢ (𝑥 ∈ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑇‘𝑚)) |
122 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚)) |
123 | 122 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚))) |
124 | 123 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
125 | 124 | rabbidv 3189 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
126 | 110 | rabex 4813 |
. . . . . . . . . . . . 13
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V |
127 | 125, 109,
126 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
128 | 127 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
129 | 128 | eleq2d 2687 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ (𝑇‘𝑚) ↔ 𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})) |
130 | 129 | biimpa 501 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
131 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑥 → (𝑠 − (𝐺‘𝑚)) = (𝑥 − (𝐺‘𝑚))) |
132 | 131 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
133 | 132 | elrab 3363 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑥 ∈ ℝ ∧ (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
134 | 130, 133 | sylib 208 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 ∈ ℝ ∧ (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
135 | 134 | simpld 475 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ∈ ℝ) |
136 | 87 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → -1 ∈ ℝ) |
137 | | iccssre 12255 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆
ℝ) |
138 | 87, 59, 137 | mp2an 708 |
. . . . . . . . . 10
⊢ (-1[,]1)
⊆ ℝ |
139 | | inss2 3834 |
. . . . . . . . . . 11
⊢ (ℚ
∩ (-1[,]1)) ⊆ (-1[,]1) |
140 | | f1of 6137 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
141 | 28, 140 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
142 | 141 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ (ℚ ∩
(-1[,]1))) |
143 | 139, 142 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ (-1[,]1)) |
144 | 138, 143 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℝ) |
145 | 144 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ∈ ℝ) |
146 | 143 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ∈ (-1[,]1)) |
147 | 87, 59 | elicc2i 12239 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑚) ∈ (-1[,]1) ↔ ((𝐺‘𝑚) ∈ ℝ ∧ -1 ≤ (𝐺‘𝑚) ∧ (𝐺‘𝑚) ≤ 1)) |
148 | 146, 147 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) ∈ ℝ ∧ -1 ≤ (𝐺‘𝑚) ∧ (𝐺‘𝑚) ≤ 1)) |
149 | 148 | simp2d 1074 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → -1 ≤ (𝐺‘𝑚)) |
150 | 27 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ran 𝐹 ⊆ (0[,]1)) |
151 | 134 | simprd 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹) |
152 | 150, 151 | sseldd 3604 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 − (𝐺‘𝑚)) ∈ (0[,]1)) |
153 | 58, 59 | elicc2i 12239 |
. . . . . . . . . . 11
⊢ ((𝑥 − (𝐺‘𝑚)) ∈ (0[,]1) ↔ ((𝑥 − (𝐺‘𝑚)) ∈ ℝ ∧ 0 ≤ (𝑥 − (𝐺‘𝑚)) ∧ (𝑥 − (𝐺‘𝑚)) ≤ 1)) |
154 | 152, 153 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝑥 − (𝐺‘𝑚)) ∈ ℝ ∧ 0 ≤ (𝑥 − (𝐺‘𝑚)) ∧ (𝑥 − (𝐺‘𝑚)) ≤ 1)) |
155 | 154 | simp2d 1074 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 0 ≤ (𝑥 − (𝐺‘𝑚))) |
156 | 135, 145 | subge0d 10617 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (0 ≤ (𝑥 − (𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ 𝑥)) |
157 | 155, 156 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ≤ 𝑥) |
158 | 136, 145,
135, 149, 157 | letrd 10194 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → -1 ≤ 𝑥) |
159 | | peano2re 10209 |
. . . . . . . . 9
⊢ ((𝐺‘𝑚) ∈ ℝ → ((𝐺‘𝑚) + 1) ∈ ℝ) |
160 | 145, 159 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) + 1) ∈ ℝ) |
161 | | 2re 11090 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
162 | 161 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 2 ∈ ℝ) |
163 | 154 | simp3d 1075 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 − (𝐺‘𝑚)) ≤ 1) |
164 | | 1red 10055 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 1 ∈ ℝ) |
165 | 135, 145,
164 | lesubadd2d 10626 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝑥 − (𝐺‘𝑚)) ≤ 1 ↔ 𝑥 ≤ ((𝐺‘𝑚) + 1))) |
166 | 163, 165 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ≤ ((𝐺‘𝑚) + 1)) |
167 | 148 | simp3d 1075 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ≤ 1) |
168 | 145, 164,
164, 167 | leadd1dd 10641 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) + 1) ≤ (1 + 1)) |
169 | | df-2 11079 |
. . . . . . . . 9
⊢ 2 = (1 +
1) |
170 | 168, 169 | syl6breqr 4695 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) + 1) ≤ 2) |
171 | 135, 160,
162, 166, 170 | letrd 10194 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ≤ 2) |
172 | 87, 161 | elicc2i 12239 |
. . . . . . 7
⊢ (𝑥 ∈ (-1[,]2) ↔ (𝑥 ∈ ℝ ∧ -1 ≤
𝑥 ∧ 𝑥 ≤ 2)) |
173 | 135, 158,
171, 172 | syl3anbrc 1246 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ∈ (-1[,]2)) |
174 | 173 | ex 450 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ (𝑇‘𝑚) → 𝑥 ∈ (-1[,]2))) |
175 | 174 | rexlimdva 3031 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ ℕ 𝑥 ∈ (𝑇‘𝑚) → 𝑥 ∈ (-1[,]2))) |
176 | 121, 175 | syl5bi 232 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) → 𝑥 ∈ (-1[,]2))) |
177 | 176 | ssrdv 3609 |
. 2
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)) |
178 | 27, 120, 177 | 3jca 1242 |
1
⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))) |