Step | Hyp | Ref
| Expression |
1 | | simprlr 780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑚)) |
2 | | simprll 779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 ∈ ℕ) |
3 | | fveq2 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚)) |
4 | 3 | oveq2d 7180 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚))) |
5 | 4 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
6 | 5 | rabbidv 3380 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
7 | | vitali.6 |
. . . . . . . . . . . . . 14
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹}) |
8 | | reex 10699 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
9 | 8 | rabex 5197 |
. . . . . . . . . . . . . 14
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V |
10 | 6, 7, 9 | fvmpt 6769 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
11 | 2, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
12 | 1, 11 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
13 | | oveq1 7171 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑚))) |
14 | 13 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
15 | 14 | elrab 3585 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
16 | 12, 15 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
17 | 16 | simpld 498 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℝ) |
18 | 17 | recnd 10740 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℂ) |
19 | | vitali.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
20 | | f1of 6612 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
22 | | inss1 4117 |
. . . . . . . . . . . 12
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℚ |
23 | | fss 6515 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ⟶(ℚ ∩
(-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℚ) → 𝐺:ℕ⟶ℚ) |
24 | 21, 22, 23 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶ℚ) |
25 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ⟶ℚ) |
26 | 25, 2 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℚ) |
27 | | qcn 12438 |
. . . . . . . . 9
⊢ ((𝐺‘𝑚) ∈ ℚ → (𝐺‘𝑚) ∈ ℂ) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℂ) |
29 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑘 ∈ ℕ) |
30 | 25, 29 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℚ) |
31 | | qcn 12438 |
. . . . . . . . 9
⊢ ((𝐺‘𝑘) ∈ ℚ → (𝐺‘𝑘) ∈ ℂ) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℂ) |
33 | | vitali.1 |
. . . . . . . . . . . . 13
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
34 | 33 | vitalilem1 24353 |
. . . . . . . . . . . 12
⊢ ∼ Er
(0[,]1) |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∼ Er
(0[,]1)) |
36 | | vitali.2 |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = ((0[,]1) / ∼
) |
37 | | vitali.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 Fn 𝑆) |
38 | | vitali.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
39 | | vitali.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol)) |
40 | 33, 36, 37, 38, 19, 7, 39 | vitalilem2 24354 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))) |
41 | 40 | simp1d 1143 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1)) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ran 𝐹 ⊆ (0[,]1)) |
43 | 16 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹) |
44 | 42, 43 | sseldd 3876 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ (0[,]1)) |
45 | | simprrr 782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑘)) |
46 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
47 | 46 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑘))) |
48 | 47 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
49 | 48 | rabbidv 3380 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
50 | 8 | rabex 5197 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ∈ V |
51 | 49, 7, 50 | fvmpt 6769 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
52 | 29, 51 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
53 | 45, 52 | eleqtrd 2835 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
54 | | oveq1 7171 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑘)) = (𝑤 − (𝐺‘𝑘))) |
55 | 54 | eleq1d 2817 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
56 | 55 | elrab 3585 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
57 | 53, 56 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
58 | 57 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹) |
59 | 42, 58 | sseldd 3876 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) |
60 | 18, 28, 32 | nnncan1d 11102 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) = ((𝐺‘𝑘) − (𝐺‘𝑚))) |
61 | | qsubcl 12443 |
. . . . . . . . . . . . . 14
⊢ (((𝐺‘𝑘) ∈ ℚ ∧ (𝐺‘𝑚) ∈ ℚ) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ) |
62 | 30, 26, 61 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ) |
63 | 60, 62 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ) |
64 | | oveq12 7173 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → (𝑥 − 𝑦) = ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘)))) |
65 | 64 | eleq1d 2817 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → ((𝑥 − 𝑦) ∈ ℚ ↔ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)) |
66 | 65, 33 | brab2a 5609 |
. . . . . . . . . . . 12
⊢ ((𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)) ↔ (((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) ∧ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)) |
67 | 44, 59, 63, 66 | syl21anbrc 1345 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘))) |
68 | 35, 67 | erthi 8364 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → [(𝑤 − (𝐺‘𝑚))] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ ) |
69 | 68 | fveq2d 6672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ )) |
70 | | eceq1 8351 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑚))] ∼ ) |
71 | 70 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ )) |
72 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → 𝑧 = (𝑤 − (𝐺‘𝑚))) |
73 | 71, 72 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))) |
74 | | fveq2 6668 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[𝑣] ∼ ) = (𝐹‘𝑤)) |
75 | 74 | eceq1d 8352 |
. . . . . . . . . . . . . . . 16
⊢ ([𝑣] ∼ = 𝑤 → [(𝐹‘[𝑣] ∼ )] ∼ =
[(𝐹‘𝑤)] ∼ ) |
76 | 75 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) =
(𝐹‘[(𝐹‘𝑤)] ∼ )) |
77 | 76, 74 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ ([𝑣] ∼ = 𝑤 → ((𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) =
(𝐹‘[𝑣] ∼ ) ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
78 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∼ Er
(0[,]1)) |
79 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1)) |
80 | | erdm 8323 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ( ∼ Er
(0[,]1) → dom ∼ =
(0[,]1)) |
81 | 34, 80 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom ∼ =
(0[,]1) |
82 | 81 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈
(0[,]1)) |
83 | | ecdmn0 8360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠
∅) |
84 | 82, 83 | bitr3i 280 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠
∅) |
85 | 79, 84 | sylib 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠
∅) |
86 | | neeq1 2996 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠
∅)) |
87 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ )) |
88 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ ) |
89 | 87, 88 | eleq12d 2827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )) |
90 | 86, 89 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
91 | 38 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
92 | | ovex 7197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0[,]1)
∈ V |
93 | | erex 8337 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ( ∼ Er
(0[,]1) → ((0[,]1) ∈ V → ∼ ∈
V)) |
94 | 34, 92, 93 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∼ ∈
V |
95 | 94 | ecelqsi 8377 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1)
/ ∼ )) |
96 | 95, 36 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ 𝑆) |
97 | 96 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆) |
98 | 90, 91, 97 | rspcdva 3526 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )) |
99 | 85, 98 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ) |
100 | | fvex 6681 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹‘[𝑣] ∼ ) ∈
V |
101 | | vex 3401 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑣 ∈ V |
102 | 100, 101 | elec 8357 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ )) |
103 | 99, 102 | sylib 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∼ (𝐹‘[𝑣] ∼ )) |
104 | 78, 103 | erthi 8364 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ = [(𝐹‘[𝑣] ∼ )] ∼
) |
105 | 104 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [(𝐹‘[𝑣] ∼ )] ∼ =
[𝑣] ∼ ) |
106 | 105 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) =
(𝐹‘[𝑣] ∼ )) |
107 | 36, 77, 106 | ectocld 8388 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)) |
108 | 107 | ralrimiva 3096 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)) |
109 | | eceq1 8351 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑤) → [𝑧] ∼ = [(𝐹‘𝑤)] ∼ ) |
110 | 109 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑤) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ )) |
111 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑤) → 𝑧 = (𝐹‘𝑤)) |
112 | 110, 111 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐹‘𝑤) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
113 | 112 | ralrn 6858 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝑆 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
114 | 37, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
115 | 108, 114 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧) |
116 | 115 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧) |
117 | 73, 116, 43 | rspcdva 3526 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚))) |
118 | | eceq1 8351 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ ) |
119 | 118 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ )) |
120 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → 𝑧 = (𝑤 − (𝐺‘𝑘))) |
121 | 119, 120 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))) |
122 | 121, 116,
58 | rspcdva 3526 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘))) |
123 | 69, 117, 122 | 3eqtr3d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑘))) |
124 | 18, 28, 32, 123 | subcand 11109 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) = (𝐺‘𝑘)) |
125 | 19 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
126 | | f1of1 6611 |
. . . . . . . . 9
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1))) |
127 | 125, 126 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1))) |
128 | | f1fveq 7025 |
. . . . . . . 8
⊢ ((𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘)) |
129 | 127, 2, 29, 128 | syl12anc 836 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘)) |
130 | 124, 129 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 = 𝑘) |
131 | 130 | ex 416 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘)) |
132 | 131 | alrimivv 1934 |
. . . 4
⊢ (𝜑 → ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘)) |
133 | | eleq1w 2815 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
134 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (𝑇‘𝑚) = (𝑇‘𝑘)) |
135 | 134 | eleq2d 2818 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝑤 ∈ (𝑇‘𝑚) ↔ 𝑤 ∈ (𝑇‘𝑘))) |
136 | 133, 135 | anbi12d 634 |
. . . . 5
⊢ (𝑚 = 𝑘 → ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) |
137 | 136 | mo4 2566 |
. . . 4
⊢
(∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘)) |
138 | 132, 137 | sylibr 237 |
. . 3
⊢ (𝜑 → ∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚))) |
139 | 138 | alrimiv 1933 |
. 2
⊢ (𝜑 → ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚))) |
140 | | dfdisj2 4994 |
. 2
⊢
(Disj 𝑚
∈ ℕ (𝑇‘𝑚) ↔ ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚))) |
141 | 139, 140 | sylibr 237 |
1
⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚)) |