Theorem infrpgernmpt

Description: The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infrpgernmpt.x	$$⊢Ⅎx\phi$$
	infrpgernmpt.a	$$⊢\phi \to A\ne \varnothing$$
	infrpgernmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
	infrpgernmpt.y	$$⊢\phi \to \exists y\in ℝ\forall x\in Ay\le B$$
	infrpgernmpt.c	$$⊢\phi \to C\in {ℝ}^{+}$$
Assertion	infrpgernmpt	$$⊢\phi \to \exists x\in AB\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$

Proof

Step	Hyp	Ref	Expression
1		infrpgernmpt.x	$$⊢Ⅎx\phi$$
2		infrpgernmpt.a	$$⊢\phi \to A\ne \varnothing$$
3		infrpgernmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
4		infrpgernmpt.y	$$⊢\phi \to \exists y\in ℝ\forall x\in Ay\le B$$
5		infrpgernmpt.c	$$⊢\phi \to C\in {ℝ}^{+}$$
6		nfv	$$⊢Ⅎw\phi$$
7		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
8	1 7 3	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq {ℝ}^{*}$$
9	1 3 7 2	rnmptn0	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing$$
10		breq1	$$⊢y=w\to \left(y\le B\leftrightarrow w\le B\right)$$
11	10	ralbidv	$$⊢y=w\to \left(\forall x\in Ay\le B\leftrightarrow \forall x\in Aw\le B\right)$$
12	11	cbvrexvw	$$⊢\exists y\in ℝ\forall x\in Ay\le B\leftrightarrow \exists w\in ℝ\forall x\in Aw\le B$$
13	4 12	sylib	$$⊢\phi \to \exists w\in ℝ\forall x\in Aw\le B$$
14	13	rnmptlb	$$⊢\phi \to \exists w\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)w\le z$$
15	6 8 9 14 5	infrpge	$$⊢\phi \to \exists w\in \mathrm{ran}\left(x\in A⟼B\right)w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
16		simpll	$$⊢\left(\left(\phi \wedge w\in \mathrm{ran}\left(x\in A⟼B\right)\right)\wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\to \phi$$
17		simpr	$$⊢\left(\left(\phi \wedge w\in \mathrm{ran}\left(x\in A⟼B\right)\right)\wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\to w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
18		vex	$$⊢w\in \mathrm{V}$$
19	7	elrnmpt	$$⊢w\in \mathrm{V}\to \left(w\in \mathrm{ran}\left(x\in A⟼B\right)\leftrightarrow \exists x\in Aw=B\right)$$
20	18 19	ax-mp	$$⊢w\in \mathrm{ran}\left(x\in A⟼B\right)\leftrightarrow \exists x\in Aw=B$$
21	20	biimpi	$$⊢w\in \mathrm{ran}\left(x\in A⟼B\right)\to \exists x\in Aw=B$$
22	21	ad2antlr	$$⊢\left(\left(\phi \wedge w\in \mathrm{ran}\left(x\in A⟼B\right)\right)\wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\to \exists x\in Aw=B$$
23		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
24		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
25		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)$$
26	25	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}\left(x\in A⟼B\right)$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}x{ℝ}^{*}$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
29	26 27 28	nfinf	$$⊢\underset{\_}{Ⅎ}xsup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}x{+}_{𝑒}$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
32	29 30 31	nfov	$$⊢\underset{\_}{Ⅎ}x\left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)$$
33	23 24 32	nfbr	$$⊢Ⅎxw\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
34	1 33	nfan	$$⊢Ⅎx\left(\phi \wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)$$
35		id	$$⊢w=B\to w=B$$
36	35	eqcomd	$$⊢w=B\to B=w$$
37	36	adantl	$$⊢\left(w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\wedge w=B\right)\to B=w$$
38		simpl	$$⊢\left(w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\wedge w=B\right)\to w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
39	37 38	eqbrtrd	$$⊢\left(w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\wedge w=B\right)\to B\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
40	39	ex	$$⊢w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\to \left(w=B\to B\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)$$
41	40	a1d	$$⊢w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\to \left(x\in A\to \left(w=B\to B\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\right)$$
42	41	adantl	$$⊢\left(\phi \wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\to \left(x\in A\to \left(w=B\to B\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\right)$$
43	34 42	reximdai	$$⊢\left(\phi \wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\to \left(\exists x\in Aw=B\to \exists x\in AB\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)$$
44	43	imp	$$⊢\left(\left(\phi \wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\wedge \exists x\in Aw=B\right)\to \exists x\in AB\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
45	16 17 22 44	syl21anc	$$⊢\left(\left(\phi \wedge w\in \mathrm{ran}\left(x\in A⟼B\right)\right)\wedge w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)\to \exists x\in AB\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$
46	45	rexlimdva2	$$⊢\phi \to \left(\exists w\in \mathrm{ran}\left(x\in A⟼B\right)w\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\to \exists x\in AB\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C\right)$$
47	15 46	mpd	$$⊢\phi \to \exists x\in AB\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right){+}_{𝑒}C$$