Theorem infxrlbrnmpt2

Description: A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	infxrlbrnmpt2.x	$$⊢Ⅎx\phi$$
	infxrlbrnmpt2.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
	infxrlbrnmpt2.c	$$⊢\phi \to C\in A$$
	infxrlbrnmpt2.d	$$⊢\phi \to D\in {ℝ}^{*}$$
	infxrlbrnmpt2.e	$$⊢x=C\to B=D$$
Assertion	infxrlbrnmpt2	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le D$$

Proof

Step	Hyp	Ref	Expression
1		infxrlbrnmpt2.x	$$⊢Ⅎx\phi$$
2		infxrlbrnmpt2.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
3		infxrlbrnmpt2.c	$$⊢\phi \to C\in A$$
4		infxrlbrnmpt2.d	$$⊢\phi \to D\in {ℝ}^{*}$$
5		infxrlbrnmpt2.e	$$⊢x=C\to B=D$$
6		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
7	1 6 2	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq {ℝ}^{*}$$
8	6 5	elrnmpt1s	$$⊢\left(C\in A\wedge D\in {ℝ}^{*}\right)\to D\in \mathrm{ran}\left(x\in A⟼B\right)$$
9	3 4 8	syl2anc	$$⊢\phi \to D\in \mathrm{ran}\left(x\in A⟼B\right)$$
10		infxrlb	$$⊢\left(\mathrm{ran}\left(x\in A⟼B\right)\subseteq {ℝ}^{*}\wedge D\in \mathrm{ran}\left(x\in A⟼B\right)\right)\to sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le D$$
11	7 9 10	syl2anc	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le D$$