Step | Hyp | Ref
| Expression |
1 | | vitali.3 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝑆) |
2 | | vitali.4 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
3 | | vitali.2 |
. . . . . . . . 9
⊢ 𝑆 = ((0[,]1) / ∼
) |
4 | | neeq1 2844 |
. . . . . . . . 9
⊢ ([𝑣] ∼ = 𝑧 → ([𝑣] ∼ ≠ ∅ ↔
𝑧 ≠
∅)) |
5 | | vitali.1 |
. . . . . . . . . . . . . 14
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
6 | 5 | vitalilem1 23182 |
. . . . . . . . . . . . 13
⊢ ∼ Er
(0[,]1) |
7 | | erdm 7639 |
. . . . . . . . . . . . 13
⊢ ( ∼ Er
(0[,]1) → dom ∼ =
(0[,]1)) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom ∼ =
(0[,]1) |
9 | 8 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈
(0[,]1)) |
10 | | ecdmn0 7676 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠
∅) |
11 | 9, 10 | bitr3i 265 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠
∅) |
12 | 11 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ≠
∅) |
13 | 3, 4, 12 | ectocl 7702 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → 𝑧 ≠ ∅) |
14 | 13 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ≠ ∅) |
15 | | sseq1 3589 |
. . . . . . . . . 10
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ (0[,]1)
↔ 𝑧 ⊆
(0[,]1))) |
16 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (0[,]1) → ∼ Er
(0[,]1)) |
17 | 16 | ecss 7675 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (0[,]1) → [𝑤] ∼ ⊆
(0[,]1)) |
18 | 3, 15, 17 | ectocl 7702 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑆 → 𝑧 ⊆ (0[,]1)) |
19 | 18 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ⊆ (0[,]1)) |
20 | 19 | sseld 3567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑧) ∈ 𝑧 → (𝐹‘𝑧) ∈ (0[,]1))) |
21 | 14, 20 | embantd 57 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → (𝐹‘𝑧) ∈ (0[,]1))) |
22 | 21 | ralimdva 2945 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
23 | 2, 22 | mpd 15 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1)) |
24 | | ffnfv 6295 |
. . . 4
⊢ (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ (0[,]1))) |
25 | 1, 23, 24 | sylanbrc 695 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶(0[,]1)) |
26 | | frn 5966 |
. . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
30 | | f1ocnv 6062 |
. . . . . . . 8
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → ◡𝐺:(ℚ ∩ (-1[,]1))–1-1-onto→ℕ) |
31 | | f1of 6050 |
. . . . . . . 8
⊢ (◡𝐺:(ℚ ∩ (-1[,]1))–1-1-onto→ℕ → ◡𝐺:(ℚ ∩
(-1[,]1))⟶ℕ) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ◡𝐺:(ℚ ∩
(-1[,]1))⟶ℕ) |
33 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (0[,]1)
∈ V |
34 | | erex 7653 |
. . . . . . . . . . . . . . 15
⊢ ( ∼ Er
(0[,]1) → ((0[,]1) ∈ V → ∼ ∈
V)) |
35 | 6, 33, 34 | mp2 9 |
. . . . . . . . . . . . . 14
⊢ ∼ ∈
V |
36 | 35 | ecelqsi 7690 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1)
/ ∼ )) |
37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ ((0[,]1)
/ ∼ )) |
38 | 37, 3 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆) |
39 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
40 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1)) |
41 | 40, 11 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠
∅) |
42 | | neeq1 2844 |
. . . . . . . . . . . . 13
⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠
∅)) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ )) |
44 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ ) |
45 | 43, 44 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )) |
46 | 42, 45 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
47 | 46 | rspcv 3278 |
. . . . . . . . . . 11
⊢ ([𝑣] ∼ ∈ 𝑆 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
48 | 38, 39, 41, 47 | syl3c 64 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ) |
49 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐹‘[𝑣] ∼ ) ∈
V |
50 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
51 | 49, 50 | elec 7673 |
. . . . . . . . . . 11
⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ )) |
52 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = (𝐹‘[𝑣] ∼ )) → (𝑥 − 𝑦) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
53 | 52 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = (𝐹‘[𝑣] ∼ )) → ((𝑥 − 𝑦) ∈ ℚ ↔ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
54 | 53, 5 | brab2ga 5117 |
. . . . . . . . . . 11
⊢ (𝑣 ∼ (𝐹‘[𝑣] ∼ ) ↔ ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈ (0[,]1))
∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
55 | 51, 54 | bitri 263 |
. . . . . . . . . 10
⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈ (0[,]1))
∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
56 | 48, 55 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈ (0[,]1))
∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ)) |
57 | 56 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℚ) |
58 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
59 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
60 | 58, 59 | elicc2i 12110 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (0[,]1) ↔ (𝑣 ∈ ℝ ∧ 0 ≤
𝑣 ∧ 𝑣 ≤ 1)) |
61 | 40, 60 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣 ∧ 𝑣 ≤ 1)) |
62 | 61 | simp1d 1066 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ ℝ) |
63 | 56 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 ∈ (0[,]1) ∧ (𝐹‘[𝑣] ∼ ) ∈
(0[,]1))) |
64 | 63 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈
(0[,]1)) |
65 | 58, 59 | elicc2i 12110 |
. . . . . . . . . . . 12
⊢ ((𝐹‘[𝑣] ∼ ) ∈ (0[,]1)
↔ ((𝐹‘[𝑣] ∼ ) ∈ ℝ
∧ 0 ≤ (𝐹‘[𝑣] ∼ ) ∧ (𝐹‘[𝑣] ∼ ) ≤
1)) |
66 | 64, 65 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) ∈ ℝ
∧ 0 ≤ (𝐹‘[𝑣] ∼ ) ∧ (𝐹‘[𝑣] ∼ ) ≤
1)) |
67 | 66 | simp1d 1066 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈
ℝ) |
68 | 62, 67 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
ℝ) |
69 | 67, 62 | resubcld 10337 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) − 𝑣) ∈
ℝ) |
70 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 1 ∈
ℝ) |
71 | 61 | simp2d 1067 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 0 ≤ 𝑣) |
72 | 67, 62 | subge02d 10498 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (0 ≤ 𝑣 ↔ ((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ (𝐹‘[𝑣] ∼
))) |
73 | 71, 72 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ (𝐹‘[𝑣] ∼ )) |
74 | 66 | simp3d 1068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ≤
1) |
75 | 69, 67, 70, 73, 74 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ 1) |
76 | 69, 70 | lenegd 10485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (((𝐹‘[𝑣] ∼ ) − 𝑣) ≤ 1 ↔ -1 ≤ -((𝐹‘[𝑣] ∼ ) − 𝑣))) |
77 | 75, 76 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → -1 ≤ -((𝐹‘[𝑣] ∼ ) − 𝑣)) |
78 | 67 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈
ℂ) |
79 | 62 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ ℂ) |
80 | 78, 79 | negsubdi2d 10287 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → -((𝐹‘[𝑣] ∼ ) − 𝑣) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
81 | 77, 80 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → -1 ≤ (𝑣 − (𝐹‘[𝑣] ∼
))) |
82 | 66 | simp2d 1067 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 0 ≤ (𝐹‘[𝑣] ∼ )) |
83 | 62, 67 | subge02d 10498 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (0 ≤ (𝐹‘[𝑣] ∼ ) ↔ (𝑣 − (𝐹‘[𝑣] ∼ )) ≤ 𝑣)) |
84 | 82, 83 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ≤ 𝑣) |
85 | 61 | simp3d 1068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ≤ 1) |
86 | 68, 62, 70, 84, 85 | letrd 10073 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ≤
1) |
87 | | neg1rr 11002 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
88 | 87, 59 | elicc2i 12110 |
. . . . . . . . 9
⊢ ((𝑣 − (𝐹‘[𝑣] ∼ )) ∈ (-1[,]1)
↔ ((𝑣 − (𝐹‘[𝑣] ∼ )) ∈ ℝ
∧ -1 ≤ (𝑣 −
(𝐹‘[𝑣] ∼ )) ∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ≤
1)) |
89 | 68, 81, 86, 88 | syl3anbrc 1239 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈
(-1[,]1)) |
90 | 57, 89 | elind 3760 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐹‘[𝑣] ∼ )) ∈ (ℚ
∩ (-1[,]1))) |
91 | 32, 90 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈
ℕ) |
92 | | f1ocnvfv2 6433 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ (𝑣 − (𝐹‘[𝑣] ∼ )) ∈ (ℚ
∩ (-1[,]1))) → (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
93 | 29, 90, 92 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = (𝑣 − (𝐹‘[𝑣] ∼
))) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) = (𝑣 − (𝑣 − (𝐹‘[𝑣] ∼
)))) |
95 | 79, 78 | nncand 10276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝑣 − (𝐹‘[𝑣] ∼ ))) = (𝐹‘[𝑣] ∼ )) |
96 | 94, 95 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) = (𝐹‘[𝑣] ∼ )) |
97 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝐹 Fn 𝑆) |
98 | | fnfvelrn 6264 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝑆 ∧ [𝑣] ∼ ∈ 𝑆) → (𝐹‘[𝑣] ∼ ) ∈ ran 𝐹) |
99 | 97, 38, 98 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ ran 𝐹) |
100 | 96, 99 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹) |
101 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑣 → (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) = (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
)))))) |
102 | 101 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑠 = 𝑣 → ((𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹 ↔ (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹)) |
103 | 102 | elrab 3331 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹} ↔ (𝑣 ∈ ℝ ∧ (𝑣 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹)) |
104 | 62, 100, 103 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
105 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → (𝐺‘𝑛) = (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
))))) |
106 | 105 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
)))))) |
107 | 106 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹)) |
108 | 107 | rabbidv 3164 |
. . . . . . . . 9
⊢ (𝑛 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
109 | | vitali.6 |
. . . . . . . . 9
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹}) |
110 | | reex 9906 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
111 | 110 | rabex 4740 |
. . . . . . . . 9
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹} ∈
V |
112 | 108, 109,
111 | fvmpt 6191 |
. . . . . . . 8
⊢ ((◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈ ℕ
→ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
113 | 91, 112 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ )))) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) ∈ ran
𝐹}) |
114 | 104, 113 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
))))) |
115 | 91, 114 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ((◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈ ℕ
∧ 𝑣 ∈ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
)))))) |
116 | | fveq2 6103 |
. . . . . 6
⊢ (𝑚 = (◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) → (𝑇‘𝑚) = (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼
))))) |
117 | 116 | eliuni 4462 |
. . . . 5
⊢ (((◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))) ∈ ℕ
∧ 𝑣 ∈ (𝑇‘(◡𝐺‘(𝑣 − (𝐹‘[𝑣] ∼ ))))) → 𝑣 ∈ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) |
118 | 115, 117 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ ∪
𝑚 ∈ ℕ (𝑇‘𝑚)) |
119 | 118 | ex 449 |
. . 3
⊢ (𝜑 → (𝑣 ∈ (0[,]1) → 𝑣 ∈ ∪
𝑚 ∈ ℕ (𝑇‘𝑚))) |
120 | 119 | ssrdv 3574 |
. 2
⊢ (𝜑 → (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) |
121 | | eliun 4460 |
. . . 4
⊢ (𝑥 ∈ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑇‘𝑚)) |
122 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚)) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚))) |
124 | 123 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
125 | 124 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
126 | 110 | rabex 4740 |
. . . . . . . . . . . . 13
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V |
127 | 125, 109,
126 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
128 | 127 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
129 | 128 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ (𝑇‘𝑚) ↔ 𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})) |
130 | 129 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
131 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑥 → (𝑠 − (𝐺‘𝑚)) = (𝑥 − (𝐺‘𝑚))) |
132 | 131 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
133 | 132 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑥 ∈ ℝ ∧ (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
134 | 130, 133 | sylib 207 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 ∈ ℝ ∧ (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
135 | 134 | simpld 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ∈ ℝ) |
136 | 87 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → -1 ∈ ℝ) |
137 | | iccssre 12126 |
. . . . . . . . . . 11
⊢ ((-1
∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆
ℝ) |
138 | 87, 59, 137 | mp2an 704 |
. . . . . . . . . 10
⊢ (-1[,]1)
⊆ ℝ |
139 | | inss2 3796 |
. . . . . . . . . . 11
⊢ (ℚ
∩ (-1[,]1)) ⊆ (-1[,]1) |
140 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
141 | 28, 140 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
142 | 141 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ (ℚ ∩
(-1[,]1))) |
143 | 139, 142 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ (-1[,]1)) |
144 | 138, 143 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℝ) |
145 | 144 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ∈ ℝ) |
146 | 143 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ∈ (-1[,]1)) |
147 | 87, 59 | elicc2i 12110 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑚) ∈ (-1[,]1) ↔ ((𝐺‘𝑚) ∈ ℝ ∧ -1 ≤ (𝐺‘𝑚) ∧ (𝐺‘𝑚) ≤ 1)) |
148 | 146, 147 | sylib 207 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) ∈ ℝ ∧ -1 ≤ (𝐺‘𝑚) ∧ (𝐺‘𝑚) ≤ 1)) |
149 | 148 | simp2d 1067 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → -1 ≤ (𝐺‘𝑚)) |
150 | 27 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ran 𝐹 ⊆ (0[,]1)) |
151 | 134 | simprd 478 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 − (𝐺‘𝑚)) ∈ ran 𝐹) |
152 | 150, 151 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 − (𝐺‘𝑚)) ∈ (0[,]1)) |
153 | 58, 59 | elicc2i 12110 |
. . . . . . . . . . 11
⊢ ((𝑥 − (𝐺‘𝑚)) ∈ (0[,]1) ↔ ((𝑥 − (𝐺‘𝑚)) ∈ ℝ ∧ 0 ≤ (𝑥 − (𝐺‘𝑚)) ∧ (𝑥 − (𝐺‘𝑚)) ≤ 1)) |
154 | 152, 153 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝑥 − (𝐺‘𝑚)) ∈ ℝ ∧ 0 ≤ (𝑥 − (𝐺‘𝑚)) ∧ (𝑥 − (𝐺‘𝑚)) ≤ 1)) |
155 | 154 | simp2d 1067 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 0 ≤ (𝑥 − (𝐺‘𝑚))) |
156 | 135, 145 | subge0d 10496 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (0 ≤ (𝑥 − (𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ 𝑥)) |
157 | 155, 156 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ≤ 𝑥) |
158 | 136, 145,
135, 149, 157 | letrd 10073 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → -1 ≤ 𝑥) |
159 | | peano2re 10088 |
. . . . . . . . 9
⊢ ((𝐺‘𝑚) ∈ ℝ → ((𝐺‘𝑚) + 1) ∈ ℝ) |
160 | 145, 159 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) + 1) ∈ ℝ) |
161 | | 2re 10967 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
162 | 161 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 2 ∈ ℝ) |
163 | 154 | simp3d 1068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝑥 − (𝐺‘𝑚)) ≤ 1) |
164 | | 1red 9934 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 1 ∈ ℝ) |
165 | 135, 145,
164 | lesubadd2d 10505 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝑥 − (𝐺‘𝑚)) ≤ 1 ↔ 𝑥 ≤ ((𝐺‘𝑚) + 1))) |
166 | 163, 165 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ≤ ((𝐺‘𝑚) + 1)) |
167 | 148 | simp3d 1068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → (𝐺‘𝑚) ≤ 1) |
168 | 145, 164,
164, 167 | leadd1dd 10520 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) + 1) ≤ (1 + 1)) |
169 | | df-2 10956 |
. . . . . . . . 9
⊢ 2 = (1 +
1) |
170 | 168, 169 | syl6breqr 4625 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → ((𝐺‘𝑚) + 1) ≤ 2) |
171 | 135, 160,
162, 166, 170 | letrd 10073 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ≤ 2) |
172 | 87, 161 | elicc2i 12110 |
. . . . . . 7
⊢ (𝑥 ∈ (-1[,]2) ↔ (𝑥 ∈ ℝ ∧ -1 ≤
𝑥 ∧ 𝑥 ≤ 2)) |
173 | 135, 158,
171, 172 | syl3anbrc 1239 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑥 ∈ (𝑇‘𝑚)) → 𝑥 ∈ (-1[,]2)) |
174 | 173 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑥 ∈ (𝑇‘𝑚) → 𝑥 ∈ (-1[,]2))) |
175 | 174 | rexlimdva 3013 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ ℕ 𝑥 ∈ (𝑇‘𝑚) → 𝑥 ∈ (-1[,]2))) |
176 | 121, 175 | syl5bi 231 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) → 𝑥 ∈ (-1[,]2))) |
177 | 176 | ssrdv 3574 |
. 2
⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)) |
178 | 27, 120, 177 | 3jca 1235 |
1
⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))) |