Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. 2
⊢ (0[,]1)
∈ V |
2 | | elpwi 4117 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
𝑦 ⊆
ℕ) |
3 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
4 | 3 | sumeq1i 14276 |
. . . . . 6
⊢
Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) |
5 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
6 | | rpnnen2.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) |
7 | 6 | rpnnen2lem6 14787 |
. . . . . . 7
⊢ ((𝑦 ⊆ ℕ ∧ 1 ∈
ℕ) → Σ𝑘
∈ (ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ∈ ℝ) |
8 | 5, 7 | mpan2 703 |
. . . . . 6
⊢ (𝑦 ⊆ ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ∈ ℝ) |
9 | 4, 8 | syl5eqel 2692 |
. . . . 5
⊢ (𝑦 ⊆ ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ∈ ℝ) |
10 | 2, 9 | syl 17 |
. . . 4
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ∈ ℝ) |
11 | | 1zzd 11285 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
1 ∈ ℤ) |
12 | | eqidd 2611 |
. . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈ ℕ) →
((𝐹‘𝑦)‘𝑘) = ((𝐹‘𝑦)‘𝑘)) |
13 | 6 | rpnnen2lem2 14783 |
. . . . . . 7
⊢ (𝑦 ⊆ ℕ → (𝐹‘𝑦):ℕ⟶ℝ) |
14 | 2, 13 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 ℕ →
(𝐹‘𝑦):ℕ⟶ℝ) |
15 | 14 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈ ℕ) →
((𝐹‘𝑦)‘𝑘) ∈ ℝ) |
16 | 6 | rpnnen2lem5 14786 |
. . . . . 6
⊢ ((𝑦 ⊆ ℕ ∧ 1 ∈
ℕ) → seq1( + , (𝐹‘𝑦)) ∈ dom ⇝ ) |
17 | 2, 5, 16 | sylancl 693 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
seq1( + , (𝐹‘𝑦)) ∈ dom ⇝
) |
18 | | ssid 3587 |
. . . . . . . 8
⊢ ℕ
⊆ ℕ |
19 | 6 | rpnnen2lem4 14785 |
. . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ ℕ
⊆ ℕ ∧ 𝑘
∈ ℕ) → (0 ≤ ((𝐹‘𝑦)‘𝑘) ∧ ((𝐹‘𝑦)‘𝑘) ≤ ((𝐹‘ℕ)‘𝑘))) |
20 | 18, 19 | mp3an2 1404 |
. . . . . . 7
⊢ ((𝑦 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → (0 ≤
((𝐹‘𝑦)‘𝑘) ∧ ((𝐹‘𝑦)‘𝑘) ≤ ((𝐹‘ℕ)‘𝑘))) |
21 | 20 | simpld 474 |
. . . . . 6
⊢ ((𝑦 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → 0 ≤
((𝐹‘𝑦)‘𝑘)) |
22 | 2, 21 | sylan 487 |
. . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈ ℕ) → 0
≤ ((𝐹‘𝑦)‘𝑘)) |
23 | 3, 11, 12, 15, 17, 22 | isumge0 14339 |
. . . 4
⊢ (𝑦 ∈ 𝒫 ℕ →
0 ≤ Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘)) |
24 | | halfre 11123 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
(1 / 2) ∈ ℝ) |
26 | | 1re 9918 |
. . . . . 6
⊢ 1 ∈
ℝ |
27 | 26 | a1i 11 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
1 ∈ ℝ) |
28 | 6 | rpnnen2lem7 14788 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ ℕ ∧ ℕ
⊆ ℕ ∧ 1 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘)) |
29 | 18, 5, 28 | mp3an23 1408 |
. . . . . . . 8
⊢ (𝑦 ⊆ ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘)) |
30 | 2, 29 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘)) |
31 | | eqid 2610 |
. . . . . . . 8
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
32 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈
(ℤ≥‘1)) → ((𝐹‘ℕ)‘𝑘) = ((𝐹‘ℕ)‘𝑘)) |
33 | | elnnuz 11600 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
34 | 6 | rpnnen2lem2 14783 |
. . . . . . . . . . . . 13
⊢ (ℕ
⊆ ℕ → (𝐹‘ℕ):ℕ⟶ℝ) |
35 | 18, 34 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐹‘ℕ):ℕ⟶ℝ |
36 | 35 | ffvelrni 6266 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((𝐹‘ℕ)‘𝑘) ∈
ℝ) |
37 | 36 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝐹‘ℕ)‘𝑘) ∈
ℂ) |
38 | 33, 37 | sylbir 224 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘1) → ((𝐹‘ℕ)‘𝑘) ∈ ℂ) |
39 | 38 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈
(ℤ≥‘1)) → ((𝐹‘ℕ)‘𝑘) ∈ ℂ) |
40 | 6 | rpnnen2lem3 14784 |
. . . . . . . . 9
⊢ seq1( + ,
(𝐹‘ℕ)) ⇝
(1 / 2) |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 ℕ →
seq1( + , (𝐹‘ℕ)) ⇝ (1 /
2)) |
42 | 31, 11, 32, 39, 41 | isumclim 14330 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘) = (1 / 2)) |
43 | 30, 42 | breqtrd 4609 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ (1 / 2)) |
44 | 4, 43 | syl5eqbr 4618 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ≤ (1 / 2)) |
45 | | halflt1 11127 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
46 | 24, 26, 45 | ltleii 10039 |
. . . . . 6
⊢ (1 / 2)
≤ 1 |
47 | 46 | a1i 11 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
(1 / 2) ≤ 1) |
48 | 10, 25, 27, 44, 47 | letrd 10073 |
. . . 4
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ≤ 1) |
49 | | 0re 9919 |
. . . . 5
⊢ 0 ∈
ℝ |
50 | 49, 26 | elicc2i 12110 |
. . . 4
⊢
(Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) ∈ (0[,]1) ↔ (Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) ∧ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) ≤ 1)) |
51 | 10, 23, 48, 50 | syl3anbrc 1239 |
. . 3
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ∈ (0[,]1)) |
52 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝒫 ℕ →
𝑧 ⊆
ℕ) |
53 | | ssdifss 3703 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ℕ → (𝑦 ∖ 𝑧) ⊆ ℕ) |
54 | | ssdifss 3703 |
. . . . . . . . . . . 12
⊢ (𝑧 ⊆ ℕ → (𝑧 ∖ 𝑦) ⊆ ℕ) |
55 | | unss 3749 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∖ 𝑧) ⊆ ℕ ∧ (𝑧 ∖ 𝑦) ⊆ ℕ) ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) |
56 | 55 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∖ 𝑧) ⊆ ℕ ∧ (𝑧 ∖ 𝑦) ⊆ ℕ) → ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) |
57 | 53, 54, 56 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) → ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) |
58 | 2, 52, 57 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) |
59 | | eqss 3583 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 ↔ (𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
60 | | ssdif0 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ 𝑧 ↔ (𝑦 ∖ 𝑧) = ∅) |
61 | | ssdif0 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑧 ∖ 𝑦) = ∅) |
62 | 60, 61 | anbi12i 729 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦) ↔ ((𝑦 ∖ 𝑧) = ∅ ∧ (𝑧 ∖ 𝑦) = ∅)) |
63 | | un00 3963 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∖ 𝑧) = ∅ ∧ (𝑧 ∖ 𝑦) = ∅) ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) = ∅) |
64 | 59, 62, 63 | 3bitri 285 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) = ∅) |
65 | 64 | necon3bii 2834 |
. . . . . . . . . . 11
⊢ (𝑦 ≠ 𝑧 ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ≠ ∅) |
66 | 65 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑦 ≠ 𝑧 → ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ≠ ∅) |
67 | | nnwo 11629 |
. . . . . . . . . 10
⊢ ((((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ ∧ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ≠ ∅) → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛) |
68 | 58, 66, 67 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
∧ 𝑦 ≠ 𝑧) → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛) |
69 | 68 | ex 449 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛)) |
70 | 58 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
∧ 𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) → 𝑚 ∈ ℕ) |
71 | | df-ral 2901 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 ↔ ∀𝑛(𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛)) |
72 | | con34b 305 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛) ↔ (¬ 𝑚 ≤ 𝑛 → ¬ 𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)))) |
73 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝑦 ∖ 𝑧) ↔ (𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧)) |
74 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝑧 ∖ 𝑦) ↔ (𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦)) |
75 | 73, 74 | orbi12i 542 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (𝑦 ∖ 𝑧) ∨ 𝑛 ∈ (𝑧 ∖ 𝑦)) ↔ ((𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧) ∨ (𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦))) |
76 | | elun 3715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ↔ (𝑛 ∈ (𝑦 ∖ 𝑧) ∨ 𝑛 ∈ (𝑧 ∖ 𝑦))) |
77 | | xor 931 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧) ↔ ((𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧) ∨ (𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦))) |
78 | 75, 76, 77 | 3bitr4ri 292 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧) ↔ 𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) |
79 | 78 | con1bii 345 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ↔ (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) |
80 | 79 | imbi2i 325 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑚 ≤ 𝑛 → ¬ 𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) ↔ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
81 | 72, 80 | bitri 263 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛) ↔ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
82 | 81 | albii 1737 |
. . . . . . . . . . . 12
⊢
(∀𝑛(𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛) ↔ ∀𝑛(¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
83 | 71, 82 | bitri 263 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 ↔ ∀𝑛(¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
84 | | alral 2912 |
. . . . . . . . . . . 12
⊢
(∀𝑛(¬
𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ∀𝑛 ∈ ℕ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
85 | | nnre 10904 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
86 | | nnre 10904 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
87 | | ltnle 9996 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑛 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑛)) |
88 | 85, 86, 87 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑛 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑛)) |
89 | 88 | imbi1d 330 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → ((𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ↔ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
90 | 89 | ralbidva 2968 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ →
(∀𝑛 ∈ ℕ
(𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ↔ ∀𝑛 ∈ ℕ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
91 | 84, 90 | syl5ibr 235 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(∀𝑛(¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
92 | 83, 91 | syl5bi 231 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
(∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
93 | 70, 92 | syl 17 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
∧ 𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) → (∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
94 | 93 | reximdva 3000 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (∃𝑚 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
95 | 69, 94 | syld 46 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
96 | | rexun 3755 |
. . . . . . 7
⊢
(∃𝑚 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ↔ (∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) |
97 | 95, 96 | syl6ib 240 |
. . . . . 6
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → (∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))))) |
98 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑦 ⊆ ℕ) |
99 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑧 ⊆ ℕ) |
100 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑚 ∈ (𝑦 ∖ 𝑧)) |
101 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
102 | | biid 250 |
. . . . . . . . . 10
⊢
(Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) |
103 | 6, 98, 99, 100, 101, 102 | rpnnen2lem11 14792 |
. . . . . . . . 9
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) |
104 | 103 | rexlimdvaa 3014 |
. . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) →
(∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) |
105 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑧 ⊆ ℕ) |
106 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑦 ⊆ ℕ) |
107 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑚 ∈ (𝑧 ∖ 𝑦)) |
108 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
109 | | bicom 211 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦) ↔ (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) |
110 | 109 | imbi2i 325 |
. . . . . . . . . . . 12
⊢ ((𝑛 < 𝑚 → (𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦)) ↔ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
111 | 110 | ralbii 2963 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦)) ↔ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) |
112 | 108, 111 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦))) |
113 | | eqcom 2617 |
. . . . . . . . . 10
⊢
(Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘)) |
114 | 6, 105, 106, 107, 112, 113 | rpnnen2lem11 14792 |
. . . . . . . . 9
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) |
115 | 114 | rexlimdvaa 3014 |
. . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) →
(∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) |
116 | 104, 115 | jaod 394 |
. . . . . . 7
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) →
((∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) |
117 | 2, 52, 116 | syl2an 493 |
. . . . . 6
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ ((∃𝑚 ∈
(𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) |
118 | 97, 117 | syld 46 |
. . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) |
119 | 118 | necon4ad 2801 |
. . . 4
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) → 𝑦 = 𝑧)) |
120 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
121 | 120 | fveq1d 6105 |
. . . . 5
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦)‘𝑘) = ((𝐹‘𝑧)‘𝑘)) |
122 | 121 | sumeq2sdv 14282 |
. . . 4
⊢ (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) |
123 | 119, 122 | impbid1 214 |
. . 3
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) ↔ 𝑦 = 𝑧)) |
124 | 51, 123 | dom2 7884 |
. 2
⊢ ((0[,]1)
∈ V → 𝒫 ℕ ≼ (0[,]1)) |
125 | 1, 124 | ax-mp 5 |
1
⊢ 𝒫
ℕ ≼ (0[,]1) |