This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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