Theorem suprubrnmpt2

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

	Ref	Expression
Hypotheses	suprubrnmpt2.x	$$⊢Ⅎx\phi$$
	suprubrnmpt2.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	suprubrnmpt2.l	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
	suprubrnmpt2.c	$$⊢\phi \to C\in A$$
	suprubrnmpt2.d	$$⊢\phi \to D\in ℝ$$
	suprubrnmpt2.i	$$⊢x=C\to B=D$$
Assertion	suprubrnmpt2	$$⊢\phi \to D\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		suprubrnmpt2.x	$$⊢Ⅎx\phi$$
2		suprubrnmpt2.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
3		suprubrnmpt2.l	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
4		suprubrnmpt2.c	$$⊢\phi \to C\in A$$
5		suprubrnmpt2.d	$$⊢\phi \to D\in ℝ$$
6		suprubrnmpt2.i	$$⊢x=C\to B=D$$
7		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
8	1 7 2	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq ℝ$$
9	7 6	elrnmpt1s	$$⊢\left(C\in A\wedge D\in ℝ\right)\to D\in \mathrm{ran}\left(x\in A⟼B\right)$$
10	4 5 9	syl2anc	$$⊢\phi \to D\in \mathrm{ran}\left(x\in A⟼B\right)$$
11	10	ne0d	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing$$
12	1 3	rnmptbdd	$$⊢\phi \to \exists y\in ℝ\forall w\in \mathrm{ran}\left(x\in A⟼B\right)w\le y$$
13	8 11 12 10	suprubd	$$⊢\phi \to D\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)$$