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	|- F/ x ph
	rexabsle2.2	|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion	rexabsle2	|- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. y e. RR A. x e. A B <_ y /\ E. y e. RR A. x e. A y <_ B ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexabsle2.1	|- F/ x ph
2		rexabsle2.2	|- ( ( ph /\ x e. A ) -> B e. RR )
3	1 2	rexabsle	|- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. y e. RR A. x e. A B <_ y /\ E. y e. RR A. x e. A y <_ B ) ) )