Theorem suprubrnmpt

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	suprubrnmpt.x	$$⊢Ⅎx\phi$$
	suprubrnmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	suprubrnmpt.e	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
Assertion	suprubrnmpt	$$⊢\left(\phi \wedge x\in A\right)\to B\le sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)$$

Proof

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