Theorem rexabsle2

Description: An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	rexabsle2.1	$$⊢Ⅎx\phi$$
	rexabsle2.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
Assertion	rexabsle2	$$⊢\phi \to \left(\exists y\in ℝ\forall x\in A\left|B\right|\le y\leftrightarrow \left(\exists y\in ℝ\forall x\in AB\le y\wedge \exists y\in ℝ\forall x\in Ay\le B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rexabsle2.1	$$⊢Ⅎx\phi$$
2		rexabsle2.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
3	1 2	rexabsle	$$⊢\phi \to \left(\exists y\in ℝ\forall x\in A\left|B\right|\le y\leftrightarrow \left(\exists y\in ℝ\forall x\in AB\le y\wedge \exists y\in ℝ\forall x\in Ay\le B\right)\right)$$