| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovex 7464 | . 2
⊢ (0[,]1)
∈ V | 
| 2 |  | elpwi 4607 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
𝑦 ⊆
ℕ) | 
| 3 |  | nnuz 12921 | . . . . . . 7
⊢ ℕ =
(ℤ≥‘1) | 
| 4 | 3 | sumeq1i 15733 | . . . . . 6
⊢
Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) | 
| 5 |  | 1nn 12277 | . . . . . . 7
⊢ 1 ∈
ℕ | 
| 6 |  | rpnnen2.1 | . . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) | 
| 7 | 6 | rpnnen2lem6 16255 | . . . . . . 7
⊢ ((𝑦 ⊆ ℕ ∧ 1 ∈
ℕ) → Σ𝑘
∈ (ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ∈ ℝ) | 
| 8 | 5, 7 | mpan2 691 | . . . . . 6
⊢ (𝑦 ⊆ ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ∈ ℝ) | 
| 9 | 4, 8 | eqeltrid 2845 | . . . . 5
⊢ (𝑦 ⊆ ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ∈ ℝ) | 
| 10 | 2, 9 | syl 17 | . . . 4
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ∈ ℝ) | 
| 11 |  | 1zzd 12648 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
1 ∈ ℤ) | 
| 12 |  | eqidd 2738 | . . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈ ℕ) →
((𝐹‘𝑦)‘𝑘) = ((𝐹‘𝑦)‘𝑘)) | 
| 13 | 6 | rpnnen2lem2 16251 | . . . . . . 7
⊢ (𝑦 ⊆ ℕ → (𝐹‘𝑦):ℕ⟶ℝ) | 
| 14 | 2, 13 | syl 17 | . . . . . 6
⊢ (𝑦 ∈ 𝒫 ℕ →
(𝐹‘𝑦):ℕ⟶ℝ) | 
| 15 | 14 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈ ℕ) →
((𝐹‘𝑦)‘𝑘) ∈ ℝ) | 
| 16 | 6 | rpnnen2lem5 16254 | . . . . . 6
⊢ ((𝑦 ⊆ ℕ ∧ 1 ∈
ℕ) → seq1( + , (𝐹‘𝑦)) ∈ dom ⇝ ) | 
| 17 | 2, 5, 16 | sylancl 586 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
seq1( + , (𝐹‘𝑦)) ∈ dom ⇝
) | 
| 18 |  | ssid 4006 | . . . . . . . 8
⊢ ℕ
⊆ ℕ | 
| 19 | 6 | rpnnen2lem4 16253 | . . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ ℕ
⊆ ℕ ∧ 𝑘
∈ ℕ) → (0 ≤ ((𝐹‘𝑦)‘𝑘) ∧ ((𝐹‘𝑦)‘𝑘) ≤ ((𝐹‘ℕ)‘𝑘))) | 
| 20 | 18, 19 | mp3an2 1451 | . . . . . . 7
⊢ ((𝑦 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → (0 ≤
((𝐹‘𝑦)‘𝑘) ∧ ((𝐹‘𝑦)‘𝑘) ≤ ((𝐹‘ℕ)‘𝑘))) | 
| 21 | 20 | simpld 494 | . . . . . 6
⊢ ((𝑦 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → 0 ≤
((𝐹‘𝑦)‘𝑘)) | 
| 22 | 2, 21 | sylan 580 | . . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈ ℕ) → 0
≤ ((𝐹‘𝑦)‘𝑘)) | 
| 23 | 3, 11, 12, 15, 17, 22 | isumge0 15802 | . . . 4
⊢ (𝑦 ∈ 𝒫 ℕ →
0 ≤ Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘)) | 
| 24 |  | halfre 12480 | . . . . . 6
⊢ (1 / 2)
∈ ℝ | 
| 25 | 24 | a1i 11 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
(1 / 2) ∈ ℝ) | 
| 26 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 27 | 26 | a1i 11 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
1 ∈ ℝ) | 
| 28 | 6 | rpnnen2lem7 16256 | . . . . . . . . 9
⊢ ((𝑦 ⊆ ℕ ∧ ℕ
⊆ ℕ ∧ 1 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘)) | 
| 29 | 18, 5, 28 | mp3an23 1455 | . . . . . . . 8
⊢ (𝑦 ⊆ ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘)) | 
| 30 | 2, 29 | syl 17 | . . . . . . 7
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘)) | 
| 31 |  | eqid 2737 | . . . . . . . 8
⊢
(ℤ≥‘1) =
(ℤ≥‘1) | 
| 32 |  | eqidd 2738 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈
(ℤ≥‘1)) → ((𝐹‘ℕ)‘𝑘) = ((𝐹‘ℕ)‘𝑘)) | 
| 33 |  | elnnuz 12922 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) | 
| 34 | 6 | rpnnen2lem2 16251 | . . . . . . . . . . . . 13
⊢ (ℕ
⊆ ℕ → (𝐹‘ℕ):ℕ⟶ℝ) | 
| 35 | 18, 34 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (𝐹‘ℕ):ℕ⟶ℝ | 
| 36 | 35 | ffvelcdmi 7103 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((𝐹‘ℕ)‘𝑘) ∈
ℝ) | 
| 37 | 36 | recnd 11289 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝐹‘ℕ)‘𝑘) ∈
ℂ) | 
| 38 | 33, 37 | sylbir 235 | . . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘1) → ((𝐹‘ℕ)‘𝑘) ∈ ℂ) | 
| 39 | 38 | adantl 481 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑘 ∈
(ℤ≥‘1)) → ((𝐹‘ℕ)‘𝑘) ∈ ℂ) | 
| 40 | 6 | rpnnen2lem3 16252 | . . . . . . . . 9
⊢ seq1( + ,
(𝐹‘ℕ)) ⇝
(1 / 2) | 
| 41 | 40 | a1i 11 | . . . . . . . 8
⊢ (𝑦 ∈ 𝒫 ℕ →
seq1( + , (𝐹‘ℕ)) ⇝ (1 /
2)) | 
| 42 | 31, 11, 32, 39, 41 | isumclim 15793 | . . . . . . 7
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘ℕ)‘𝑘) = (1 / 2)) | 
| 43 | 30, 42 | breqtrd 5169 | . . . . . 6
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈
(ℤ≥‘1)((𝐹‘𝑦)‘𝑘) ≤ (1 / 2)) | 
| 44 | 4, 43 | eqbrtrid 5178 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ≤ (1 / 2)) | 
| 45 |  | halflt1 12484 | . . . . . . 7
⊢ (1 / 2)
< 1 | 
| 46 | 24, 26, 45 | ltleii 11384 | . . . . . 6
⊢ (1 / 2)
≤ 1 | 
| 47 | 46 | a1i 11 | . . . . 5
⊢ (𝑦 ∈ 𝒫 ℕ →
(1 / 2) ≤ 1) | 
| 48 | 10, 25, 27, 44, 47 | letrd 11418 | . . . 4
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ≤ 1) | 
| 49 |  | elicc01 13506 | . . . 4
⊢
(Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) ∈ (0[,]1) ↔ (Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) ∧ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) ≤ 1)) | 
| 50 | 10, 23, 48, 49 | syl3anbrc 1344 | . . 3
⊢ (𝑦 ∈ 𝒫 ℕ →
Σ𝑘 ∈ ℕ
((𝐹‘𝑦)‘𝑘) ∈ (0[,]1)) | 
| 51 |  | elpwi 4607 | . . . . . . . . . . 11
⊢ (𝑧 ∈ 𝒫 ℕ →
𝑧 ⊆
ℕ) | 
| 52 |  | ssdifss 4140 | . . . . . . . . . . . 12
⊢ (𝑦 ⊆ ℕ → (𝑦 ∖ 𝑧) ⊆ ℕ) | 
| 53 |  | ssdifss 4140 | . . . . . . . . . . . 12
⊢ (𝑧 ⊆ ℕ → (𝑧 ∖ 𝑦) ⊆ ℕ) | 
| 54 |  | unss 4190 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∖ 𝑧) ⊆ ℕ ∧ (𝑧 ∖ 𝑦) ⊆ ℕ) ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) | 
| 55 | 54 | biimpi 216 | . . . . . . . . . . . 12
⊢ (((𝑦 ∖ 𝑧) ⊆ ℕ ∧ (𝑧 ∖ 𝑦) ⊆ ℕ) → ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) | 
| 56 | 52, 53, 55 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) → ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) | 
| 57 | 2, 51, 56 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ) | 
| 58 |  | eqss 3999 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 ↔ (𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦)) | 
| 59 |  | ssdif0 4366 | . . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ 𝑧 ↔ (𝑦 ∖ 𝑧) = ∅) | 
| 60 |  | ssdif0 4366 | . . . . . . . . . . . . . 14
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑧 ∖ 𝑦) = ∅) | 
| 61 | 59, 60 | anbi12i 628 | . . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦) ↔ ((𝑦 ∖ 𝑧) = ∅ ∧ (𝑧 ∖ 𝑦) = ∅)) | 
| 62 |  | un00 4445 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∖ 𝑧) = ∅ ∧ (𝑧 ∖ 𝑦) = ∅) ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) = ∅) | 
| 63 | 58, 61, 62 | 3bitri 297 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) = ∅) | 
| 64 | 63 | necon3bii 2993 | . . . . . . . . . . 11
⊢ (𝑦 ≠ 𝑧 ↔ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ≠ ∅) | 
| 65 | 64 | biimpi 216 | . . . . . . . . . 10
⊢ (𝑦 ≠ 𝑧 → ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ≠ ∅) | 
| 66 |  | nnwo 12955 | . . . . . . . . . 10
⊢ ((((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ⊆ ℕ ∧ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ≠ ∅) → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛) | 
| 67 | 57, 65, 66 | syl2an 596 | . . . . . . . . 9
⊢ (((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
∧ 𝑦 ≠ 𝑧) → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛) | 
| 68 | 67 | ex 412 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛)) | 
| 69 | 57 | sselda 3983 | . . . . . . . . . 10
⊢ (((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
∧ 𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) → 𝑚 ∈ ℕ) | 
| 70 |  | df-ral 3062 | . . . . . . . . . . . 12
⊢
(∀𝑛 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 ↔ ∀𝑛(𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛)) | 
| 71 |  | con34b 316 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛) ↔ (¬ 𝑚 ≤ 𝑛 → ¬ 𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)))) | 
| 72 |  | eldif 3961 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝑦 ∖ 𝑧) ↔ (𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧)) | 
| 73 |  | eldif 3961 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (𝑧 ∖ 𝑦) ↔ (𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦)) | 
| 74 | 72, 73 | orbi12i 915 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (𝑦 ∖ 𝑧) ∨ 𝑛 ∈ (𝑧 ∖ 𝑦)) ↔ ((𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧) ∨ (𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦))) | 
| 75 |  | elun 4153 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ↔ (𝑛 ∈ (𝑦 ∖ 𝑧) ∨ 𝑛 ∈ (𝑧 ∖ 𝑦))) | 
| 76 |  | xor 1017 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧) ↔ ((𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧) ∨ (𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦))) | 
| 77 | 74, 75, 76 | 3bitr4ri 304 | . . . . . . . . . . . . . . . 16
⊢ (¬
(𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧) ↔ 𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) | 
| 78 | 77 | con1bii 356 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) ↔ (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) | 
| 79 | 78 | imbi2i 336 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑚 ≤ 𝑛 → ¬ 𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) ↔ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 80 | 71, 79 | bitri 275 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛) ↔ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 81 | 80 | albii 1819 | . . . . . . . . . . . 12
⊢
(∀𝑛(𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦)) → 𝑚 ≤ 𝑛) ↔ ∀𝑛(¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 82 | 70, 81 | bitri 275 | . . . . . . . . . . 11
⊢
(∀𝑛 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 ↔ ∀𝑛(¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 83 |  | alral 3075 | . . . . . . . . . . . 12
⊢
(∀𝑛(¬
𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ∀𝑛 ∈ ℕ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 84 |  | nnre 12273 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) | 
| 85 |  | nnre 12273 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) | 
| 86 |  | ltnle 11340 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑛 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑛)) | 
| 87 | 84, 85, 86 | syl2anr 597 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑛 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑛)) | 
| 88 | 87 | imbi1d 341 | . . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → ((𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ↔ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 89 | 88 | ralbidva 3176 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ →
(∀𝑛 ∈ ℕ
(𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ↔ ∀𝑛 ∈ ℕ (¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 90 | 83, 89 | imbitrrid 246 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(∀𝑛(¬ 𝑚 ≤ 𝑛 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 91 | 82, 90 | biimtrid 242 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
(∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 92 | 69, 91 | syl 17 | . . . . . . . . 9
⊢ (((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
∧ 𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))) → (∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 93 | 92 | reximdva 3168 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (∃𝑚 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))𝑚 ≤ 𝑛 → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 94 | 68, 93 | syld 47 | . . . . . . 7
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → ∃𝑚 ∈ ((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 95 |  | rexun 4196 | . . . . . . 7
⊢
(∃𝑚 ∈
((𝑦 ∖ 𝑧) ∪ (𝑧 ∖ 𝑦))∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ↔ (∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) | 
| 96 | 94, 95 | imbitrdi 251 | . . . . . 6
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → (∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))))) | 
| 97 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑦 ⊆ ℕ) | 
| 98 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑧 ⊆ ℕ) | 
| 99 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑚 ∈ (𝑦 ∖ 𝑧)) | 
| 100 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 101 |  | biid 261 | . . . . . . . . . 10
⊢
(Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) | 
| 102 | 6, 97, 98, 99, 100, 101 | rpnnen2lem11 16260 | . . . . . . . . 9
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑦 ∖ 𝑧) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) | 
| 103 | 102 | rexlimdvaa 3156 | . . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) →
(∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) | 
| 104 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑧 ⊆ ℕ) | 
| 105 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑦 ⊆ ℕ) | 
| 106 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → 𝑚 ∈ (𝑧 ∖ 𝑦)) | 
| 107 |  | simprr 773 | . . . . . . . . . . 11
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 108 |  | bicom 222 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦) ↔ (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) | 
| 109 | 108 | imbi2i 336 | . . . . . . . . . . . 12
⊢ ((𝑛 < 𝑚 → (𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦)) ↔ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 110 | 109 | ralbii 3093 | . . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦)) ↔ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) | 
| 111 | 107, 110 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦))) | 
| 112 |  | eqcom 2744 | . . . . . . . . . 10
⊢
(Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘)) | 
| 113 | 6, 104, 105, 106, 111, 112 | rpnnen2lem11 16260 | . . . . . . . . 9
⊢ (((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) ∧ (𝑚 ∈ (𝑧 ∖ 𝑦) ∧ ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) | 
| 114 | 113 | rexlimdvaa 3156 | . . . . . . . 8
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) →
(∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) | 
| 115 | 103, 114 | jaod 860 | . . . . . . 7
⊢ ((𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ) →
((∃𝑚 ∈ (𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) | 
| 116 | 2, 51, 115 | syl2an 596 | . . . . . 6
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ ((∃𝑚 ∈
(𝑦 ∖ 𝑧)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧)) ∨ ∃𝑚 ∈ (𝑧 ∖ 𝑦)∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧))) → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) | 
| 117 | 96, 116 | syld 47 | . . . . 5
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (𝑦 ≠ 𝑧 → ¬ Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘))) | 
| 118 | 117 | necon4ad 2959 | . . . 4
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) → 𝑦 = 𝑧)) | 
| 119 |  | fveq2 6906 | . . . . . 6
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) | 
| 120 | 119 | fveq1d 6908 | . . . . 5
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦)‘𝑘) = ((𝐹‘𝑧)‘𝑘)) | 
| 121 | 120 | sumeq2sdv 15739 | . . . 4
⊢ (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘)) | 
| 122 | 118, 121 | impbid1 225 | . . 3
⊢ ((𝑦 ∈ 𝒫 ℕ ∧
𝑧 ∈ 𝒫 ℕ)
→ (Σ𝑘 ∈
ℕ ((𝐹‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝑧)‘𝑘) ↔ 𝑦 = 𝑧)) | 
| 123 | 50, 122 | dom2 9035 | . 2
⊢ ((0[,]1)
∈ V → 𝒫 ℕ ≼ (0[,]1)) | 
| 124 | 1, 123 | ax-mp 5 | 1
⊢ 𝒫
ℕ ≼ (0[,]1) |