Theorem rpnnen1lem6

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 15-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1lem.1	$$⊢T=\left\{n\in \mathbb{Z}|\frac{n}{k}<x\right\}$$
	rpnnen1lem.2	$$⊢F=\left(x\in ℝ⟼\left(k\in \mathbb{N}⟼\frac{sup\left(T,ℝ,<\right)}{k}\right)\right)$$
	rpnnen1lem.n	$$⊢\mathbb{N}\in \mathrm{V}$$
	rpnnen1lem.q	$$⊢\mathbb{Q}\in \mathrm{V}$$
Assertion	rpnnen1lem6	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	$$⊢T=\left\{n\in \mathbb{Z}|\frac{n}{k}<x\right\}$$
2		rpnnen1lem.2	$$⊢F=\left(x\in ℝ⟼\left(k\in \mathbb{N}⟼\frac{sup\left(T,ℝ,<\right)}{k}\right)\right)$$
3		rpnnen1lem.n	$$⊢\mathbb{N}\in \mathrm{V}$$
4		rpnnen1lem.q	$$⊢\mathbb{Q}\in \mathrm{V}$$
5		ovex	$$⊢{\mathbb{Q}}^{\mathbb{N}}\in \mathrm{V}$$
6	1 2 3 4	rpnnen1lem1	$$⊢x\in ℝ\to F\left(x\right)\in \left({\mathbb{Q}}^{\mathbb{N}}\right)$$
7		rneq	$$⊢F\left(x\right)=F\left(y\right)\to \mathrm{ran}F\left(x\right)=\mathrm{ran}F\left(y\right)$$
8	7	supeq1d	$$⊢F\left(x\right)=F\left(y\right)\to sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)=sup\left(\mathrm{ran}F\left(y\right),ℝ,<\right)$$
9	1 2 3 4	rpnnen1lem5	$$⊢x\in ℝ\to sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)=x$$
10		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
11	10	rneqd	$$⊢x=y\to \mathrm{ran}F\left(x\right)=\mathrm{ran}F\left(y\right)$$
12	11	supeq1d	$$⊢x=y\to sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)=sup\left(\mathrm{ran}F\left(y\right),ℝ,<\right)$$
13		id	$$⊢x=y\to x=y$$
14	12 13	eqeq12d	$$⊢x=y\to \left(sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)=x\leftrightarrow sup\left(\mathrm{ran}F\left(y\right),ℝ,<\right)=y\right)$$
15	14 9	vtoclga	$$⊢y\in ℝ\to sup\left(\mathrm{ran}F\left(y\right),ℝ,<\right)=y$$
16	9 15	eqeqan12d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)=sup\left(\mathrm{ran}F\left(y\right),ℝ,<\right)\leftrightarrow x=y\right)$$
17	8 16	imbitrid	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
18	17 10	impbid1	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow x=y\right)$$
19	6 18	dom2	$$⊢{\mathbb{Q}}^{\mathbb{N}}\in \mathrm{V}\to ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$
20	5 19	ax-mp	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$