Theorem rpnnen2lem12

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

	Ref	Expression
Hypothesis	rpnnen2.1	$$⊢F=\left(x\in 𝒫\mathbb{N}⟼\left(n\in \mathbb{N}⟼if\left(n\in x,{\left(\frac{1}{3}\right)}^n,0\right)\right)\right)$$
Assertion	rpnnen2lem12	$$⊢𝒫\mathbb{N}\preccurlyeq \left[0,1\right]$$

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	$$⊢F=\left(x\in 𝒫\mathbb{N}⟼\left(n\in \mathbb{N}⟼if\left(n\in x,{\left(\frac{1}{3}\right)}^n,0\right)\right)\right)$$
2		ovex	$$⊢\left[0,1\right]\in \mathrm{V}$$
3		elpwi	$$⊢y\in 𝒫\mathbb{N}\to y\subseteq \mathbb{N}$$
4		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
5	4	sumeq1i	$$⊢\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	1	rpnnen2lem6	$$⊢\left(y\subseteq \mathbb{N}\wedge 1\in \mathbb{N}\right)\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)\in ℝ$$
8	6 7	mpan2	$$⊢y\subseteq \mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)\in ℝ$$
9	5 8	eqeltrid	$$⊢y\subseteq \mathbb{N}\to \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\in ℝ$$
10	3 9	syl	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\in ℝ$$
11		1zzd	$$⊢y\in 𝒫\mathbb{N}\to 1\in \mathbb{Z}$$
12		eqidd	$$⊢\left(y\in 𝒫\mathbb{N}\wedge k\in \mathbb{N}\right)\to F\left(y\right)\left(k\right)=F\left(y\right)\left(k\right)$$
13	1	rpnnen2lem2	$$⊢y\subseteq \mathbb{N}\to F\left(y\right):\mathbb{N}⟶ℝ$$
14	3 13	syl	$$⊢y\in 𝒫\mathbb{N}\to F\left(y\right):\mathbb{N}⟶ℝ$$
15	14	ffvelcdmda	$$⊢\left(y\in 𝒫\mathbb{N}\wedge k\in \mathbb{N}\right)\to F\left(y\right)\left(k\right)\in ℝ$$
16	1	rpnnen2lem5	$$⊢\left(y\subseteq \mathbb{N}\wedge 1\in \mathbb{N}\right)\to seq1\left(+,F\left(y\right)\right)\in \mathrm{dom}⇝$$
17	3 6 16	sylancl	$$⊢y\in 𝒫\mathbb{N}\to seq1\left(+,F\left(y\right)\right)\in \mathrm{dom}⇝$$
18		ssid	$$⊢\mathbb{N}\subseteq \mathbb{N}$$
19	1	rpnnen2lem4	$$⊢\left(y\subseteq \mathbb{N}\wedge \mathbb{N}\subseteq \mathbb{N}\wedge k\in \mathbb{N}\right)\to \left(0\le F\left(y\right)\left(k\right)\wedge F\left(y\right)\left(k\right)\le F\left(\mathbb{N}\right)\left(k\right)\right)$$
20	18 19	mp3an2	$$⊢\left(y\subseteq \mathbb{N}\wedge k\in \mathbb{N}\right)\to \left(0\le F\left(y\right)\left(k\right)\wedge F\left(y\right)\left(k\right)\le F\left(\mathbb{N}\right)\left(k\right)\right)$$
21	20	simpld	$$⊢\left(y\subseteq \mathbb{N}\wedge k\in \mathbb{N}\right)\to 0\le F\left(y\right)\left(k\right)$$
22	3 21	sylan	$$⊢\left(y\in 𝒫\mathbb{N}\wedge k\in \mathbb{N}\right)\to 0\le F\left(y\right)\left(k\right)$$
23	4 11 12 15 17 22	isumge0	$$⊢y\in 𝒫\mathbb{N}\to 0\le \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)$$
24		halfre	$$⊢\frac{1}{2}\in ℝ$$
25	24	a1i	$$⊢y\in 𝒫\mathbb{N}\to \frac{1}{2}\in ℝ$$
26		1re	$$⊢1\in ℝ$$
27	26	a1i	$$⊢y\in 𝒫\mathbb{N}\to 1\in ℝ$$
28	1	rpnnen2lem7	$$⊢\left(y\subseteq \mathbb{N}\wedge \mathbb{N}\subseteq \mathbb{N}\wedge 1\in \mathbb{N}\right)\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(\mathbb{N}\right)\left(k\right)$$
29	18 6 28	mp3an23	$$⊢y\subseteq \mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(\mathbb{N}\right)\left(k\right)$$
30	3 29	syl	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)\le \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(\mathbb{N}\right)\left(k\right)$$
31		eqid	$$⊢{\mathbb{Z}}_{\ge 1}={\mathbb{Z}}_{\ge 1}$$
32		eqidd	$$⊢\left(y\in 𝒫\mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to F\left(\mathbb{N}\right)\left(k\right)=F\left(\mathbb{N}\right)\left(k\right)$$
33		elnnuz	$$⊢k\in \mathbb{N}\leftrightarrow k\in {\mathbb{Z}}_{\ge 1}$$
34	1	rpnnen2lem2	$$⊢\mathbb{N}\subseteq \mathbb{N}\to F\left(\mathbb{N}\right):\mathbb{N}⟶ℝ$$
35	18 34	ax-mp	$$⊢F\left(\mathbb{N}\right):\mathbb{N}⟶ℝ$$
36	35	ffvelcdmi	$$⊢k\in \mathbb{N}\to F\left(\mathbb{N}\right)\left(k\right)\in ℝ$$
37	36	recnd	$$⊢k\in \mathbb{N}\to F\left(\mathbb{N}\right)\left(k\right)\in ℂ$$
38	33 37	sylbir	$$⊢k\in {\mathbb{Z}}_{\ge 1}\to F\left(\mathbb{N}\right)\left(k\right)\in ℂ$$
39	38	adantl	$$⊢\left(y\in 𝒫\mathbb{N}\wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to F\left(\mathbb{N}\right)\left(k\right)\in ℂ$$
40	1	rpnnen2lem3	$$⊢seq1\left(+,F\left(\mathbb{N}\right)\right)⇝\left(\frac{1}{2}\right)$$
41	40	a1i	$$⊢y\in 𝒫\mathbb{N}\to seq1\left(+,F\left(\mathbb{N}\right)\right)⇝\left(\frac{1}{2}\right)$$
42	31 11 32 39 41	isumclim	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(\mathbb{N}\right)\left(k\right)=\frac{1}{2}$$
43	30 42	breqtrd	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(y\right)\left(k\right)\le \frac{1}{2}$$
44	5 43	eqbrtrid	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\le \frac{1}{2}$$
45		halflt1	$$⊢\frac{1}{2}<1$$
46	24 26 45	ltleii	$$⊢\frac{1}{2}\le 1$$
47	46	a1i	$$⊢y\in 𝒫\mathbb{N}\to \frac{1}{2}\le 1$$
48	10 25 27 44 47	letrd	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\le 1$$
49		elicc01	$$⊢\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\in \left[0,1\right]\leftrightarrow \left(\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\in ℝ\wedge 0\le \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\wedge \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\le 1\right)$$
50	10 23 48 49	syl3anbrc	$$⊢y\in 𝒫\mathbb{N}\to \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)\in \left[0,1\right]$$
51		elpwi	$$⊢z\in 𝒫\mathbb{N}\to z\subseteq \mathbb{N}$$
52		ssdifss	$$⊢y\subseteq \mathbb{N}\to y\setminus z\subseteq \mathbb{N}$$
53		ssdifss	$$⊢z\subseteq \mathbb{N}\to z\setminus y\subseteq \mathbb{N}$$
54		unss	$$⊢\left(y\setminus z\subseteq \mathbb{N}\wedge z\setminus y\subseteq \mathbb{N}\right)\leftrightarrow \left(y\setminus z\right)\cup \left(z\setminus y\right)\subseteq \mathbb{N}$$
55	54	biimpi	$$⊢\left(y\setminus z\subseteq \mathbb{N}\wedge z\setminus y\subseteq \mathbb{N}\right)\to \left(y\setminus z\right)\cup \left(z\setminus y\right)\subseteq \mathbb{N}$$
56	52 53 55	syl2an	$$⊢\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\to \left(y\setminus z\right)\cup \left(z\setminus y\right)\subseteq \mathbb{N}$$
57	3 51 56	syl2an	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(y\setminus z\right)\cup \left(z\setminus y\right)\subseteq \mathbb{N}$$
58		eqss	$$⊢y=z\leftrightarrow \left(y\subseteq z\wedge z\subseteq y\right)$$
59		ssdif0	$$⊢y\subseteq z\leftrightarrow y\setminus z=\varnothing$$
60		ssdif0	$$⊢z\subseteq y\leftrightarrow z\setminus y=\varnothing$$
61	59 60	anbi12i	$$⊢\left(y\subseteq z\wedge z\subseteq y\right)\leftrightarrow \left(y\setminus z=\varnothing \wedge z\setminus y=\varnothing \right)$$
62		un00	$$⊢\left(y\setminus z=\varnothing \wedge z\setminus y=\varnothing \right)\leftrightarrow \left(y\setminus z\right)\cup \left(z\setminus y\right)=\varnothing$$
63	58 61 62	3bitri	$$⊢y=z\leftrightarrow \left(y\setminus z\right)\cup \left(z\setminus y\right)=\varnothing$$
64	63	necon3bii	$$⊢y\ne z\leftrightarrow \left(y\setminus z\right)\cup \left(z\setminus y\right)\ne \varnothing$$
65	64	biimpi	$$⊢y\ne z\to \left(y\setminus z\right)\cup \left(z\setminus y\right)\ne \varnothing$$
66		nnwo	$$⊢\left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\subseteq \mathbb{N}\wedge \left(y\setminus z\right)\cup \left(z\setminus y\right)\ne \varnothing \right)\to \exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n$$
67	57 65 66	syl2an	$$⊢\left(\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\wedge y\ne z\right)\to \exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n$$
68	67	ex	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(y\ne z\to \exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n\right)$$
69	57	sselda	$$⊢\left(\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\wedge m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\right)\to m\in \mathbb{N}$$
70		df-ral	$$⊢\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n\leftrightarrow \forall n\left(n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\to m\le n\right)$$
71		con34b	$$⊢\left(n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\to m\le n\right)\leftrightarrow \left(\neg m\le n\to \neg n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\right)$$
72		eldif	$$⊢n\in \left(y\setminus z\right)\leftrightarrow \left(n\in y\wedge \neg n\in z\right)$$
73		eldif	$$⊢n\in \left(z\setminus y\right)\leftrightarrow \left(n\in z\wedge \neg n\in y\right)$$
74	72 73	orbi12i	$$⊢\left(n\in \left(y\setminus z\right)\vee n\in \left(z\setminus y\right)\right)\leftrightarrow \left(\left(n\in y\wedge \neg n\in z\right)\vee \left(n\in z\wedge \neg n\in y\right)\right)$$
75		elun	$$⊢n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\leftrightarrow \left(n\in \left(y\setminus z\right)\vee n\in \left(z\setminus y\right)\right)$$
76		xor	$$⊢\neg \left(n\in y\leftrightarrow n\in z\right)\leftrightarrow \left(\left(n\in y\wedge \neg n\in z\right)\vee \left(n\in z\wedge \neg n\in y\right)\right)$$
77	74 75 76	3bitr4ri	$$⊢\neg \left(n\in y\leftrightarrow n\in z\right)\leftrightarrow n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)$$
78	77	con1bii	$$⊢\neg n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\leftrightarrow \left(n\in y\leftrightarrow n\in z\right)$$
79	78	imbi2i	$$⊢\left(\neg m\le n\to \neg n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\right)\leftrightarrow \left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
80	71 79	bitri	$$⊢\left(n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\to m\le n\right)\leftrightarrow \left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
81	80	albii	$$⊢\forall n\left(n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\to m\le n\right)\leftrightarrow \forall n\left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
82	70 81	bitri	$$⊢\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n\leftrightarrow \forall n\left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
83		alral	$$⊢\forall n\left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)\to \forall n\in \mathbb{N}\left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
84		nnre	$$⊢n\in \mathbb{N}\to n\in ℝ$$
85		nnre	$$⊢m\in \mathbb{N}\to m\in ℝ$$
86		ltnle	$$⊢\left(n\in ℝ\wedge m\in ℝ\right)\to \left(n<m\leftrightarrow \neg m\le n\right)$$
87	84 85 86	syl2anr	$$⊢\left(m\in \mathbb{N}\wedge n\in \mathbb{N}\right)\to \left(n<m\leftrightarrow \neg m\le n\right)$$
88	87	imbi1d	$$⊢\left(m\in \mathbb{N}\wedge n\in \mathbb{N}\right)\to \left(\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\leftrightarrow \left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
89	88	ralbidva	$$⊢m\in \mathbb{N}\to \left(\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\leftrightarrow \forall n\in \mathbb{N}\left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
90	83 89	imbitrrid	$$⊢m\in \mathbb{N}\to \left(\forall n\left(\neg m\le n\to \left(n\in y\leftrightarrow n\in z\right)\right)\to \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
91	82 90	biimtrid	$$⊢m\in \mathbb{N}\to \left(\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n\to \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
92	69 91	syl	$$⊢\left(\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\wedge m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\right)\to \left(\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n\to \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
93	92	reximdva	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(\exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)m\le n\to \exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
94	68 93	syld	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(y\ne z\to \exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
95		rexun	$$⊢\exists m\in \left(\left(y\setminus z\right)\cup \left(z\setminus y\right)\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\leftrightarrow \left(\exists m\in \left(y\setminus z\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\vee \exists m\in \left(z\setminus y\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)$$
96	94 95	imbitrdi	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(y\ne z\to \left(\exists m\in \left(y\setminus z\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\vee \exists m\in \left(z\setminus y\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)$$
97		simpll	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(y\setminus z\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to y\subseteq \mathbb{N}$$
98		simplr	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(y\setminus z\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to z\subseteq \mathbb{N}$$
99		simprl	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(y\setminus z\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to m\in \left(y\setminus z\right)$$
100		simprr	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(y\setminus z\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
101		biid	$$⊢\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\leftrightarrow \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)$$
102	1 97 98 99 100 101	rpnnen2lem11	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(y\setminus z\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)$$
103	102	rexlimdvaa	$$⊢\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\to \left(\exists m\in \left(y\setminus z\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\right)$$
104		simplr	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(z\setminus y\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to z\subseteq \mathbb{N}$$
105		simpll	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(z\setminus y\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to y\subseteq \mathbb{N}$$
106		simprl	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(z\setminus y\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to m\in \left(z\setminus y\right)$$
107		simprr	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(z\setminus y\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
108		bicom	$$⊢\left(n\in z\leftrightarrow n\in y\right)\leftrightarrow \left(n\in y\leftrightarrow n\in z\right)$$
109	108	imbi2i	$$⊢\left(n<m\to \left(n\in z\leftrightarrow n\in y\right)\right)\leftrightarrow \left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
110	109	ralbii	$$⊢\forall n\in \mathbb{N}\left(n<m\to \left(n\in z\leftrightarrow n\in y\right)\right)\leftrightarrow \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)$$
111	107 110	sylibr	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(z\setminus y\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to \forall n\in \mathbb{N}\left(n<m\to \left(n\in z\leftrightarrow n\in y\right)\right)$$
112		eqcom	$$⊢\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\leftrightarrow \sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)$$
113	1 104 105 106 111 112	rpnnen2lem11	$$⊢\left(\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\wedge \left(m\in \left(z\setminus y\right)\wedge \forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\right)\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)$$
114	113	rexlimdvaa	$$⊢\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\to \left(\exists m\in \left(z\setminus y\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\right)$$
115	103 114	jaod	$$⊢\left(y\subseteq \mathbb{N}\wedge z\subseteq \mathbb{N}\right)\to \left(\left(\exists m\in \left(y\setminus z\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\vee \exists m\in \left(z\setminus y\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\right)$$
116	3 51 115	syl2an	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(\left(\exists m\in \left(y\setminus z\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\vee \exists m\in \left(z\setminus y\right)\forall n\in \mathbb{N}\left(n<m\to \left(n\in y\leftrightarrow n\in z\right)\right)\right)\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\right)$$
117	96 116	syld	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(y\ne z\to \neg \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\right)$$
118	117	necon4ad	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\to y=z\right)$$
119		fveq2	$$⊢y=z\to F\left(y\right)=F\left(z\right)$$
120	119	fveq1d	$$⊢y=z\to F\left(y\right)\left(k\right)=F\left(z\right)\left(k\right)$$
121	120	sumeq2sdv	$$⊢y=z\to \sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)$$
122	118 121	impbid1	$$⊢\left(y\in 𝒫\mathbb{N}\wedge z\in 𝒫\mathbb{N}\right)\to \left(\sum _{k\in \mathbb{N}}F\left(y\right)\left(k\right)=\sum _{k\in \mathbb{N}}F\left(z\right)\left(k\right)\leftrightarrow y=z\right)$$
123	50 122	dom2	$$⊢\left[0,1\right]\in \mathrm{V}\to 𝒫\mathbb{N}\preccurlyeq \left[0,1\right]$$
124	2 123	ax-mp	$$⊢𝒫\mathbb{N}\preccurlyeq \left[0,1\right]$$