Theorem rexabsle

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

Proof

Step	Hyp	Ref	Expression
1		rexabsle.1	|- F/ x ph
2		rexabsle.2	|- ( ( ph /\ x e. A ) -> B e. RR )
3		nfv	|- F/ x y = a
4		breq2	|- ( y = a -> ( ( abs ` B ) <_ y <-> ( abs ` B ) <_ a ) )
5	3 4	ralbid	|- ( y = a -> ( A. x e. A ( abs ` B ) <_ y <-> A. x e. A ( abs ` B ) <_ a ) )
6	5	cbvrexvw	|- ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> E. a e. RR A. x e. A ( abs ` B ) <_ a )
7	6	a1i	|- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> E. a e. RR A. x e. A ( abs ` B ) <_ a ) )
8	1 2	rexabslelem	|- ( ph -> ( E. a e. RR A. x e. A ( abs ` B ) <_ a <-> ( E. b e. RR A. x e. A B <_ b /\ E. c e. RR A. x e. A c <_ B ) ) )
9		breq2	|- ( b = w -> ( B <_ b <-> B <_ w ) )
10	9	ralbidv	|- ( b = w -> ( A. x e. A B <_ b <-> A. x e. A B <_ w ) )
11	10	cbvrexvw	|- ( E. b e. RR A. x e. A B <_ b <-> E. w e. RR A. x e. A B <_ w )
12		breq1	|- ( c = z -> ( c <_ B <-> z <_ B ) )
13	12	ralbidv	|- ( c = z -> ( A. x e. A c <_ B <-> A. x e. A z <_ B ) )
14	13	cbvrexvw	|- ( E. c e. RR A. x e. A c <_ B <-> E. z e. RR A. x e. A z <_ B )
15	11 14	anbi12i	|- ( ( E. b e. RR A. x e. A B <_ b /\ E. c e. RR A. x e. A c <_ B ) <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) )
16	15	a1i	|- ( ph -> ( ( E. b e. RR A. x e. A B <_ b /\ E. c e. RR A. x e. A c <_ B ) <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )
17	7 8 16	3bitrd	|- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )