Metamath Proof Explorer

Theorem rpnnen2lem12

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

Ref Expression
Hypothesis rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion rpnnen2lem12 𝒫 ℕ ≼ ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2 ovex ⊢ ( 0 [,] 1 ) ∈ V
3 elpwi ⊢ ( 𝑦 ∈ 𝒫 ℕ → 𝑦 ⊆ ℕ )
4 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
5 4 sumeq1i ⊢ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 )
6 1nn ⊢ 1 ∈ ℕ
7 1 rpnnen2lem6 ⊢ ( ( 𝑦 ⊆ ℕ ∧ 1 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ℝ )
8 6 7 mpan2 ⊢ ( 𝑦 ⊆ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ℝ )
9 5 8 eqeltrid ⊢ ( 𝑦 ⊆ ℕ → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ℝ )
10 3 9 syl ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ℝ )
11 1zzd ⊢ ( 𝑦 ∈ 𝒫 ℕ → 1 ∈ ℤ )
12 eqidd ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) )
13 1 rpnnen2lem2 ⊢ ( 𝑦 ⊆ ℕ → ( 𝐹 ‘ 𝑦 ) : ℕ ⟶ ℝ )
14 3 13 syl ⊢ ( 𝑦 ∈ 𝒫 ℕ → ( 𝐹 ‘ 𝑦 ) : ℕ ⟶ ℝ )
15 14 ffvelrnda ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ℝ )
16 1 rpnnen2lem5 ⊢ ( ( 𝑦 ⊆ ℕ ∧ 1 ∈ ℕ ) → seq 1 ( + , ( 𝐹 ‘ 𝑦 ) ) ∈ dom ⇝ )
17 3 6 16 sylancl ⊢ ( 𝑦 ∈ 𝒫 ℕ → seq 1 ( + , ( 𝐹 ‘ 𝑦 ) ) ∈ dom ⇝ )
18 ssid ⊢ ℕ ⊆ ℕ
19 1 rpnnen2lem4 ⊢ ( ( 𝑦 ⊆ ℕ ∧ ℕ ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) ) )
20 18 19 mp3an2 ⊢ ( ( 𝑦 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) ) )
21 20 simpld ⊢ ( ( 𝑦 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) )
22 3 21 sylan ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) )
23 4 11 12 15 17 22 isumge0 ⊢ ( 𝑦 ∈ 𝒫 ℕ → 0 ≤ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) )
24 halfre ⊢ ( 1 / 2 ) ∈ ℝ
25 24 a1i ⊢ ( 𝑦 ∈ 𝒫 ℕ → ( 1 / 2 ) ∈ ℝ )
26 1re ⊢ 1 ∈ ℝ
27 26 a1i ⊢ ( 𝑦 ∈ 𝒫 ℕ → 1 ∈ ℝ )
28 1 rpnnen2lem7 ⊢ ( ( 𝑦 ⊆ ℕ ∧ ℕ ⊆ ℕ ∧ 1 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) )
29 18 6 28 mp3an23 ⊢ ( 𝑦 ⊆ ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) )
30 3 29 syl ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) )
31 eqid ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ 1 )
32 eqidd ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) = ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) )
33 elnnuz ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
34 1 rpnnen2lem2 ⊢ ( ℕ ⊆ ℕ → ( 𝐹 ‘ ℕ ) : ℕ ⟶ ℝ )
35 18 34 ax-mp ⊢ ( 𝐹 ‘ ℕ ) : ℕ ⟶ ℝ
36 35 ffvelrni ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) ∈ ℝ )
37 36 recnd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) ∈ ℂ )
38 33 37 sylbir ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) ∈ ℂ )
39 38 adantl ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) ∈ ℂ )
40 1 rpnnen2lem3 ⊢ seq 1 ( + , ( 𝐹 ‘ ℕ ) ) ⇝ ( 1 / 2 )
41 40 a1i ⊢ ( 𝑦 ∈ 𝒫 ℕ → seq 1 ( + , ( 𝐹 ‘ ℕ ) ) ⇝ ( 1 / 2 ) )
42 31 11 32 39 41 isumclim ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ ℕ ) ‘ 𝑘 ) = ( 1 / 2 ) )
43 30 42 breqtrd ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ ( 1 / 2 ) )
44 5 43 eqbrtrid ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ ( 1 / 2 ) )
45 halflt1 ⊢ ( 1 / 2 ) < 1
46 24 26 45 ltleii ⊢ ( 1 / 2 ) ≤ 1
47 46 a1i ⊢ ( 𝑦 ∈ 𝒫 ℕ → ( 1 / 2 ) ≤ 1 )
48 10 25 27 44 47 letrd ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ 1 )
49 elicc01 ⊢ ( Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ( 0 [,] 1 ) ↔ ( Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ≤ 1 ) )
50 10 23 48 49 syl3anbrc ⊢ ( 𝑦 ∈ 𝒫 ℕ → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) ∈ ( 0 [,] 1 ) )
51 elpwi ⊢ ( 𝑧 ∈ 𝒫 ℕ → 𝑧 ⊆ ℕ )
52 ssdifss ⊢ ( 𝑦 ⊆ ℕ → ( 𝑦 ∖ 𝑧 ) ⊆ ℕ )
53 ssdifss ⊢ ( 𝑧 ⊆ ℕ → ( 𝑧 ∖ 𝑦 ) ⊆ ℕ )
54 unss ⊢ ( ( ( 𝑦 ∖ 𝑧 ) ⊆ ℕ ∧ ( 𝑧 ∖ 𝑦 ) ⊆ ℕ ) ↔ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ⊆ ℕ )
55 54 biimpi ⊢ ( ( ( 𝑦 ∖ 𝑧 ) ⊆ ℕ ∧ ( 𝑧 ∖ 𝑦 ) ⊆ ℕ ) → ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ⊆ ℕ )
56 52 53 55 syl2an ⊢ ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) → ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ⊆ ℕ )
57 3 51 56 syl2an ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ⊆ ℕ )
58 eqss ⊢ ( 𝑦 = 𝑧 ↔ ( 𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
59 ssdif0 ⊢ ( 𝑦 ⊆ 𝑧 ↔ ( 𝑦 ∖ 𝑧 ) = ∅ )
60 ssdif0 ⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑧 ∖ 𝑦 ) = ∅ )
61 59 60 anbi12i ⊢ ( ( 𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ( ( 𝑦 ∖ 𝑧 ) = ∅ ∧ ( 𝑧 ∖ 𝑦 ) = ∅ ) )
62 un00 ⊢ ( ( ( 𝑦 ∖ 𝑧 ) = ∅ ∧ ( 𝑧 ∖ 𝑦 ) = ∅ ) ↔ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) = ∅ )
63 58 61 62 3bitri ⊢ ( 𝑦 = 𝑧 ↔ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) = ∅ )
64 63 necon3bii ⊢ ( 𝑦 ≠ 𝑧 ↔ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ≠ ∅ )
65 64 biimpi ⊢ ( 𝑦 ≠ 𝑧 → ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ≠ ∅ )
66 nnwo ⊢ ( ( ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ⊆ ℕ ∧ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ≠ ∅ ) → ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 )
67 57 65 66 syl2an ⊢ ( ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) ∧ 𝑦 ≠ 𝑧 ) → ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 )
68 67 ex ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( 𝑦 ≠ 𝑧 → ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 ) )
69 57 sselda ⊢ ( ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) ∧ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ) → 𝑚 ∈ ℕ )
70 df-ral ⊢ ( ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 ↔ ∀ 𝑛 ( 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) → 𝑚 ≤ 𝑛 ) )
71 con34b ⊢ ( ( 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) → 𝑚 ≤ 𝑛 ) ↔ ( ¬ 𝑚 ≤ 𝑛 → ¬ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ) )
72 eldif ⊢ ( 𝑛 ∈ ( 𝑦 ∖ 𝑧 ) ↔ ( 𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧 ) )
73 eldif ⊢ ( 𝑛 ∈ ( 𝑧 ∖ 𝑦 ) ↔ ( 𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦 ) )
74 72 73 orbi12i ⊢ ( ( 𝑛 ∈ ( 𝑦 ∖ 𝑧 ) ∨ 𝑛 ∈ ( 𝑧 ∖ 𝑦 ) ) ↔ ( ( 𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧 ) ∨ ( 𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦 ) ) )
75 elun ⊢ ( 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ↔ ( 𝑛 ∈ ( 𝑦 ∖ 𝑧 ) ∨ 𝑛 ∈ ( 𝑧 ∖ 𝑦 ) ) )
76 xor ⊢ ( ¬ ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ↔ ( ( 𝑛 ∈ 𝑦 ∧ ¬ 𝑛 ∈ 𝑧 ) ∨ ( 𝑛 ∈ 𝑧 ∧ ¬ 𝑛 ∈ 𝑦 ) ) )
77 74 75 76 3bitr4ri ⊢ ( ¬ ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ↔ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) )
78 77 con1bii ⊢ ( ¬ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ↔ ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) )
79 78 imbi2i ⊢ ( ( ¬ 𝑚 ≤ 𝑛 → ¬ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ) ↔ ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
80 71 79 bitri ⊢ ( ( 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) → 𝑚 ≤ 𝑛 ) ↔ ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
81 80 albii ⊢ ( ∀ 𝑛 ( 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) → 𝑚 ≤ 𝑛 ) ↔ ∀ 𝑛 ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
82 70 81 bitri ⊢ ( ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 ↔ ∀ 𝑛 ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
83 alral ⊢ ( ∀ 𝑛 ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) → ∀ 𝑛 ∈ ℕ ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
84 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
85 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
86 ltnle ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( 𝑛 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑛 ) )
87 84 85 86 syl2anr ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑛 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑛 ) )
88 87 imbi1d ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ↔ ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
89 88 ralbidva ⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
90 83 89 syl5ibr ⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑛 ( ¬ 𝑚 ≤ 𝑛 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
91 82 90 syl5bi ⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
92 69 91 syl ⊢ ( ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) ∧ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ) → ( ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
93 92 reximdva ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) 𝑚 ≤ 𝑛 → ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
94 68 93 syld ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( 𝑦 ≠ 𝑧 → ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
95 rexun ⊢ ( ∃ 𝑚 ∈ ( ( 𝑦 ∖ 𝑧 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ↔ ( ∃ 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ∨ ∃ 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) )
96 94 95 syl6ib ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( 𝑦 ≠ 𝑧 → ( ∃ 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ∨ ∃ 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) )
97 simpll ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → 𝑦 ⊆ ℕ )
98 simplr ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → 𝑧 ⊆ ℕ )
99 simprl ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) )
100 simprr ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
101 biid ⊢ ( Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ↔ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) )
102 1 97 98 99 100 101 rpnnen2lem11 ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) )
103 102 rexlimdvaa ⊢ ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) → ( ∃ 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) )
104 simplr ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → 𝑧 ⊆ ℕ )
105 simpll ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → 𝑦 ⊆ ℕ )
106 simprl ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) )
107 simprr ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
108 bicom ⊢ ( ( 𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦 ) ↔ ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) )
109 108 imbi2i ⊢ ( ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦 ) ) ↔ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
110 109 ralbii ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) )
111 107 110 sylibr ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑧 ↔ 𝑛 ∈ 𝑦 ) ) )
112 eqcom ⊢ ( Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ↔ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) )
113 1 104 105 106 111 112 rpnnen2lem11 ⊢ ( ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) ∧ ( 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) ) → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) )
114 113 rexlimdvaa ⊢ ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) → ( ∃ 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) )
115 103 114 jaod ⊢ ( ( 𝑦 ⊆ ℕ ∧ 𝑧 ⊆ ℕ ) → ( ( ∃ 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ∨ ∃ 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) )
116 3 51 115 syl2an ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( ( ∃ 𝑚 ∈ ( 𝑦 ∖ 𝑧 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ∨ ∃ 𝑚 ∈ ( 𝑧 ∖ 𝑦 ) ∀ 𝑛 ∈ ℕ ( 𝑛 < 𝑚 → ( 𝑛 ∈ 𝑦 ↔ 𝑛 ∈ 𝑧 ) ) ) → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) )
117 96 116 syld ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( 𝑦 ≠ 𝑧 → ¬ Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ) )
118 117 necon4ad ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) → 𝑦 = 𝑧 ) )
119 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
120 119 fveq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) )
121 120 sumeq2sdv ⊢ ( 𝑦 = 𝑧 → Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) )
122 118 121 impbid1 ⊢ ( ( 𝑦 ∈ 𝒫 ℕ ∧ 𝑧 ∈ 𝒫 ℕ ) → ( Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑘 ) ↔ 𝑦 = 𝑧 ) )
123 50 122 dom2 ⊢ ( ( 0 [,] 1 ) ∈ V → 𝒫 ℕ ≼ ( 0 [,] 1 ) )
124 2 123 ax-mp ⊢ 𝒫 ℕ ≼ ( 0 [,] 1 )