Theorem rpnnen1lem4

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-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	rpnnen1lem4	$$⊢x\in ℝ\to sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)\in ℝ$$

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	1 2 3 4	rpnnen1lem1	$$⊢x\in ℝ\to F\left(x\right)\in \left({\mathbb{Q}}^{\mathbb{N}}\right)$$
6	4 3	elmap	$$⊢F\left(x\right)\in \left({\mathbb{Q}}^{\mathbb{N}}\right)\leftrightarrow F\left(x\right):\mathbb{N}⟶\mathbb{Q}$$
7	5 6	sylib	$$⊢x\in ℝ\to F\left(x\right):\mathbb{N}⟶\mathbb{Q}$$
8		frn	$$⊢F\left(x\right):\mathbb{N}⟶\mathbb{Q}\to \mathrm{ran}F\left(x\right)\subseteq \mathbb{Q}$$
9		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
10	8 9	sstrdi	$$⊢F\left(x\right):\mathbb{N}⟶\mathbb{Q}\to \mathrm{ran}F\left(x\right)\subseteq ℝ$$
11	7 10	syl	$$⊢x\in ℝ\to \mathrm{ran}F\left(x\right)\subseteq ℝ$$
12		1nn	$$⊢1\in \mathbb{N}$$
13	12	ne0ii	$$⊢\mathbb{N}\ne \varnothing$$
14		fdm	$$⊢F\left(x\right):\mathbb{N}⟶\mathbb{Q}\to \mathrm{dom}F\left(x\right)=\mathbb{N}$$
15	14	neeq1d	$$⊢F\left(x\right):\mathbb{N}⟶\mathbb{Q}\to \left(\mathrm{dom}F\left(x\right)\ne \varnothing \leftrightarrow \mathbb{N}\ne \varnothing \right)$$
16	13 15	mpbiri	$$⊢F\left(x\right):\mathbb{N}⟶\mathbb{Q}\to \mathrm{dom}F\left(x\right)\ne \varnothing$$
17		dm0rn0	$$⊢\mathrm{dom}F\left(x\right)=\varnothing \leftrightarrow \mathrm{ran}F\left(x\right)=\varnothing$$
18	17	necon3bii	$$⊢\mathrm{dom}F\left(x\right)\ne \varnothing \leftrightarrow \mathrm{ran}F\left(x\right)\ne \varnothing$$
19	16 18	sylib	$$⊢F\left(x\right):\mathbb{N}⟶\mathbb{Q}\to \mathrm{ran}F\left(x\right)\ne \varnothing$$
20	7 19	syl	$$⊢x\in ℝ\to \mathrm{ran}F\left(x\right)\ne \varnothing$$
21	1 2 3 4	rpnnen1lem3	$$⊢x\in ℝ\to \forall n\in \mathrm{ran}F\left(x\right)n\le x$$
22		breq2	$$⊢y=x\to \left(n\le y\leftrightarrow n\le x\right)$$
23	22	ralbidv	$$⊢y=x\to \left(\forall n\in \mathrm{ran}F\left(x\right)n\le y\leftrightarrow \forall n\in \mathrm{ran}F\left(x\right)n\le x\right)$$
24	23	rspcev	$$⊢\left(x\in ℝ\wedge \forall n\in \mathrm{ran}F\left(x\right)n\le x\right)\to \exists y\in ℝ\forall n\in \mathrm{ran}F\left(x\right)n\le y$$
25	21 24	mpdan	$$⊢x\in ℝ\to \exists y\in ℝ\forall n\in \mathrm{ran}F\left(x\right)n\le y$$
26		suprcl	$$⊢\left(\mathrm{ran}F\left(x\right)\subseteq ℝ\wedge \mathrm{ran}F\left(x\right)\ne \varnothing \wedge \exists y\in ℝ\forall n\in \mathrm{ran}F\left(x\right)n\le y\right)\to sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)\in ℝ$$
27	11 20 25 26	syl3anc	$$⊢x\in ℝ\to sup\left(\mathrm{ran}F\left(x\right),ℝ,<\right)\in ℝ$$