Step | Hyp | Ref
| Expression |
1 | | simprlr 803 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑚)) |
2 | | simprll 802 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 ∈ ℕ) |
3 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚)) |
4 | 3 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚))) |
5 | 4 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
6 | 5 | rabbidv 3189 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
7 | | vitali.6 |
. . . . . . . . . . . . . 14
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹}) |
8 | | reex 10027 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
9 | 8 | rabex 4813 |
. . . . . . . . . . . . . 14
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V |
10 | 6, 7, 9 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
11 | 2, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
12 | 1, 11 | eleqtrd 2703 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}) |
13 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑚))) |
14 | 13 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
15 | 14 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
16 | 12, 15 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹)) |
17 | 16 | simpld 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℝ) |
18 | 17 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ ℂ) |
19 | | vitali.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
20 | | f1of 6137 |
. . . . . . . . . . . . 13
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩
(-1[,]1))) |
22 | | inss1 3833 |
. . . . . . . . . . . 12
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℚ |
23 | | fss 6056 |
. . . . . . . . . . . 12
⊢ ((𝐺:ℕ⟶(ℚ ∩
(-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℚ) → 𝐺:ℕ⟶ℚ) |
24 | 21, 22, 23 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶ℚ) |
25 | 24 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ⟶ℚ) |
26 | 25, 2 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℚ) |
27 | | qcn 11802 |
. . . . . . . . 9
⊢ ((𝐺‘𝑚) ∈ ℚ → (𝐺‘𝑚) ∈ ℂ) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) ∈ ℂ) |
29 | | simprrl 804 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑘 ∈ ℕ) |
30 | 25, 29 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℚ) |
31 | | qcn 11802 |
. . . . . . . . 9
⊢ ((𝐺‘𝑘) ∈ ℚ → (𝐺‘𝑘) ∈ ℂ) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑘) ∈ ℂ) |
33 | | vitali.1 |
. . . . . . . . . . . . 13
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
34 | 33 | vitalilem1 23376 |
. . . . . . . . . . . 12
⊢ ∼ Er
(0[,]1) |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∼ Er
(0[,]1)) |
36 | | vitali.2 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = ((0[,]1) / ∼
) |
37 | | vitali.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn 𝑆) |
38 | | vitali.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
39 | | vitali.7 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ
∖ dom vol)) |
40 | 33, 36, 37, 38, 19, 7, 39 | vitalilem2 23378 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆
∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪
𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))) |
41 | 40 | simp1d 1073 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1)) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ran 𝐹 ⊆ (0[,]1)) |
43 | 16 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹) |
44 | 42, 43 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∈ (0[,]1)) |
45 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ (𝑇‘𝑘)) |
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
47 | 46 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑘))) |
48 | 47 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
49 | 48 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
50 | 8 | rabex 4813 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ∈ V |
51 | 49, 7, 50 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
52 | 29, 51 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑇‘𝑘) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
53 | 45, 52 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹}) |
54 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑤 → (𝑠 − (𝐺‘𝑘)) = (𝑤 − (𝐺‘𝑘))) |
55 | 54 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑤 → ((𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹 ↔ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
56 | 55 | elrab 3363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑘)) ∈ ran 𝐹} ↔ (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
57 | 53, 56 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 ∈ ℝ ∧ (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹)) |
58 | 57 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹) |
59 | 42, 58 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) |
60 | 44, 59 | jca 554 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1))) |
61 | 18, 28, 32 | nnncan1d 10426 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) = ((𝐺‘𝑘) − (𝐺‘𝑚))) |
62 | | qsubcl 11807 |
. . . . . . . . . . . . . 14
⊢ (((𝐺‘𝑘) ∈ ℚ ∧ (𝐺‘𝑚) ∈ ℚ) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ) |
63 | 30, 26, 62 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑘) − (𝐺‘𝑚)) ∈ ℚ) |
64 | 61, 63 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ) |
65 | | oveq12 6659 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → (𝑥 − 𝑦) = ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘)))) |
66 | 65 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝑤 − (𝐺‘𝑚)) ∧ 𝑦 = (𝑤 − (𝐺‘𝑘))) → ((𝑥 − 𝑦) ∈ ℚ ↔ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)) |
67 | 66, 33 | brab2a 5194 |
. . . . . . . . . . . 12
⊢ ((𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘)) ↔ (((𝑤 − (𝐺‘𝑚)) ∈ (0[,]1) ∧ (𝑤 − (𝐺‘𝑘)) ∈ (0[,]1)) ∧ ((𝑤 − (𝐺‘𝑚)) − (𝑤 − (𝐺‘𝑘))) ∈ ℚ)) |
68 | 60, 64, 67 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) ∼ (𝑤 − (𝐺‘𝑘))) |
69 | 35, 68 | erthi 7793 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → [(𝑤 − (𝐺‘𝑚))] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ ) |
70 | 69 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ )) |
71 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[𝑣] ∼ ) = (𝐹‘𝑤)) |
72 | 71 | eceq1d 7783 |
. . . . . . . . . . . . . . . 16
⊢ ([𝑣] ∼ = 𝑤 → [(𝐹‘[𝑣] ∼ )] ∼ =
[(𝐹‘𝑤)] ∼ ) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ([𝑣] ∼ = 𝑤 → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) =
(𝐹‘[(𝐹‘𝑤)] ∼ )) |
74 | 73, 71 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ ([𝑣] ∼ = 𝑤 → ((𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) =
(𝐹‘[𝑣] ∼ ) ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
75 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∼ Er
(0[,]1)) |
76 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0[,]1)
∈ V |
77 | | erex 7766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ( ∼ Er
(0[,]1) → ((0[,]1) ∈ V → ∼ ∈
V)) |
78 | 34, 76, 77 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∼ ∈
V |
79 | 78 | ecelqsi 7803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ ((0[,]1)
/ ∼ )) |
80 | 79, 36 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ (0[,]1) → [𝑣] ∼ ∈ 𝑆) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ∈ 𝑆) |
82 | 38 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧)) |
83 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1)) |
84 | | erdm 7752 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ( ∼ Er
(0[,]1) → dom ∼ =
(0[,]1)) |
85 | 34, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom ∼ =
(0[,]1) |
86 | 85 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ dom ∼ ↔ 𝑣 ∈
(0[,]1)) |
87 | | ecdmn0 7789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ dom ∼ ↔ [𝑣] ∼ ≠
∅) |
88 | 86, 87 | bitr3i 266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ (0[,]1) ↔ [𝑣] ∼ ≠
∅) |
89 | 83, 88 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ ≠
∅) |
90 | | neeq1 2856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = [𝑣] ∼ → (𝑧 ≠ ∅ ↔ [𝑣] ∼ ≠
∅)) |
91 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = [𝑣] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑣] ∼ )) |
92 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = [𝑣] ∼ → 𝑧 = [𝑣] ∼ ) |
93 | 91, 92 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = [𝑣] ∼ → ((𝐹‘𝑧) ∈ 𝑧 ↔ (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ )) |
94 | 90, 93 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = [𝑣] ∼ → ((𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) ↔ ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
95 | 94 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑣] ∼ ∈ 𝑆 → (∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧) → ([𝑣] ∼ ≠ ∅ →
(𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼
))) |
96 | 81, 82, 89, 95 | syl3c 66 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ) |
97 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹‘[𝑣] ∼ ) ∈
V |
98 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑣 ∈ V |
99 | 97, 98 | elec 7786 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘[𝑣] ∼ ) ∈ [𝑣] ∼ ↔ 𝑣 ∼ (𝐹‘[𝑣] ∼ )) |
100 | 96, 99 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∼ (𝐹‘[𝑣] ∼ )) |
101 | 75, 100 | erthi 7793 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [𝑣] ∼ = [(𝐹‘[𝑣] ∼ )] ∼
) |
102 | 101 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → [(𝐹‘[𝑣] ∼ )] ∼ =
[𝑣] ∼ ) |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (0[,]1)) → (𝐹‘[(𝐹‘[𝑣] ∼ )] ∼ ) =
(𝐹‘[𝑣] ∼ )) |
104 | 36, 74, 103 | ectocld 7814 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)) |
105 | 104 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤)) |
106 | | eceq1 7782 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑤) → [𝑧] ∼ = [(𝐹‘𝑤)] ∼ ) |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑤) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝐹‘𝑤)] ∼ )) |
108 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑤) → 𝑧 = (𝐹‘𝑤)) |
109 | 107, 108 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐹‘𝑤) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
110 | 109 | ralrn 6362 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝑆 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
111 | 37, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 ↔ ∀𝑤 ∈ 𝑆 (𝐹‘[(𝐹‘𝑤)] ∼ ) = (𝐹‘𝑤))) |
112 | 105, 111 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧) |
113 | 112 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧) |
114 | | eceq1 7782 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑚))] ∼ ) |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ )) |
116 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → 𝑧 = (𝑤 − (𝐺‘𝑚))) |
117 | 115, 116 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑤 − (𝐺‘𝑚)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))) |
118 | 117 | rspcv 3305 |
. . . . . . . . . 10
⊢ ((𝑤 − (𝐺‘𝑚)) ∈ ran 𝐹 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚)))) |
119 | 43, 113, 118 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑚))] ∼ ) = (𝑤 − (𝐺‘𝑚))) |
120 | | eceq1 7782 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → [𝑧] ∼ = [(𝑤 − (𝐺‘𝑘))] ∼ ) |
121 | 120 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → (𝐹‘[𝑧] ∼ ) = (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ )) |
122 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → 𝑧 = (𝑤 − (𝐺‘𝑘))) |
123 | 121, 122 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑤 − (𝐺‘𝑘)) → ((𝐹‘[𝑧] ∼ ) = 𝑧 ↔ (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))) |
124 | 123 | rspcv 3305 |
. . . . . . . . . 10
⊢ ((𝑤 − (𝐺‘𝑘)) ∈ ran 𝐹 → (∀𝑧 ∈ ran 𝐹(𝐹‘[𝑧] ∼ ) = 𝑧 → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘)))) |
125 | 58, 113, 124 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐹‘[(𝑤 − (𝐺‘𝑘))] ∼ ) = (𝑤 − (𝐺‘𝑘))) |
126 | 70, 119, 125 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝑤 − (𝐺‘𝑚)) = (𝑤 − (𝐺‘𝑘))) |
127 | 18, 28, 32, 126 | subcand 10433 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → (𝐺‘𝑚) = (𝐺‘𝑘)) |
128 | 19 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
129 | | f1of1 6136 |
. . . . . . . . 9
⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1))) |
130 | 128, 129 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1))) |
131 | | f1fveq 6519 |
. . . . . . . 8
⊢ ((𝐺:ℕ–1-1→(ℚ ∩ (-1[,]1)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘)) |
132 | 130, 2, 29, 131 | syl12anc 1324 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → ((𝐺‘𝑚) = (𝐺‘𝑘) ↔ 𝑚 = 𝑘)) |
133 | 127, 132 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) → 𝑚 = 𝑘) |
134 | 133 | ex 450 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘)) |
135 | 134 | alrimivv 1856 |
. . . 4
⊢ (𝜑 → ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘)) |
136 | | eleq1 2689 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
137 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (𝑇‘𝑚) = (𝑇‘𝑘)) |
138 | 137 | eleq2d 2687 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (𝑤 ∈ (𝑇‘𝑚) ↔ 𝑤 ∈ (𝑇‘𝑘))) |
139 | 136, 138 | anbi12d 747 |
. . . . 5
⊢ (𝑚 = 𝑘 → ((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘)))) |
140 | 139 | mo4 2517 |
. . . 4
⊢
(∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ↔ ∀𝑚∀𝑘(((𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚)) ∧ (𝑘 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑘))) → 𝑚 = 𝑘)) |
141 | 135, 140 | sylibr 224 |
. . 3
⊢ (𝜑 → ∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚))) |
142 | 141 | alrimiv 1855 |
. 2
⊢ (𝜑 → ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚))) |
143 | | dfdisj2 4622 |
. 2
⊢
(Disj 𝑚
∈ ℕ (𝑇‘𝑚) ↔ ∀𝑤∃*𝑚(𝑚 ∈ ℕ ∧ 𝑤 ∈ (𝑇‘𝑚))) |
144 | 142, 143 | sylibr 224 |
1
⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚)) |