Metamath Proof Explorer


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 ) ) )