Theorem supxrre3rnmpt

Description: The indexed supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		supxrre3rnmpt.x	$$⊢Ⅎx\phi$$
2		supxrre3rnmpt.a	$$⊢\phi \to A\ne \varnothing$$
3		supxrre3rnmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
4		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
5	1 4 3	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq ℝ$$
6	1 3 4 2	rnmptn0	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing$$
7		supxrre3	$$⊢\left(\mathrm{ran}\left(x\in A⟼B\right)\subseteq ℝ\wedge \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing \right)\to \left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\in ℝ\leftrightarrow \exists y\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)z\le y\right)$$
8	5 6 7	syl2anc	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\in ℝ\leftrightarrow \exists y\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)z\le y\right)$$
9	1 3	rnmptbd	$$⊢\phi \to \left(\exists y\in ℝ\forall x\in AB\le y\leftrightarrow \exists y\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)z\le y\right)$$
10	8 9	bitr4d	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\in ℝ\leftrightarrow \exists y\in ℝ\forall x\in AB\le y\right)$$