Metamath Proof Explorer


Theorem uzub

Description: A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses uzub.1
|- F/ j ph
uzub.2
|- ( ph -> M e. ZZ )
uzub.3
|- Z = ( ZZ>= ` M )
uzub.12
|- ( ( ph /\ j e. Z ) -> B e. RR )
Assertion uzub
|- ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. x e. RR A. j e. Z B <_ x ) )

Proof

Step Hyp Ref Expression
1 uzub.1
 |-  F/ j ph
2 uzub.2
 |-  ( ph -> M e. ZZ )
3 uzub.3
 |-  Z = ( ZZ>= ` M )
4 uzub.12
 |-  ( ( ph /\ j e. Z ) -> B e. RR )
5 fveq2
 |-  ( k = i -> ( ZZ>= ` k ) = ( ZZ>= ` i ) )
6 5 raleqdv
 |-  ( k = i -> ( A. j e. ( ZZ>= ` k ) B <_ x <-> A. j e. ( ZZ>= ` i ) B <_ x ) )
7 6 cbvrexvw
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ x )
8 7 a1i
 |-  ( x = w -> ( E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ x ) )
9 breq2
 |-  ( x = w -> ( B <_ x <-> B <_ w ) )
10 9 ralbidv
 |-  ( x = w -> ( A. j e. ( ZZ>= ` i ) B <_ x <-> A. j e. ( ZZ>= ` i ) B <_ w ) )
11 10 rexbidv
 |-  ( x = w -> ( E. i e. Z A. j e. ( ZZ>= ` i ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
12 8 11 bitrd
 |-  ( x = w -> ( E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
13 12 cbvrexvw
 |-  ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w )
14 13 a1i
 |-  ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
15 breq2
 |-  ( w = y -> ( B <_ w <-> B <_ y ) )
16 15 ralbidv
 |-  ( w = y -> ( A. j e. ( ZZ>= ` i ) B <_ w <-> A. j e. ( ZZ>= ` i ) B <_ y ) )
17 16 rexbidv
 |-  ( w = y -> ( E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y ) )
18 17 cbvrexvw
 |-  ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w <-> E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y )
19 18 biimpi
 |-  ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w -> E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y )
20 nfv
 |-  F/ j y e. RR
21 1 20 nfan
 |-  F/ j ( ph /\ y e. RR )
22 nfv
 |-  F/ j i e. Z
23 21 22 nfan
 |-  F/ j ( ( ph /\ y e. RR ) /\ i e. Z )
24 nfra1
 |-  F/ j A. j e. ( ZZ>= ` i ) B <_ y
25 23 24 nfan
 |-  F/ j ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y )
26 nfmpt1
 |-  F/_ j ( j e. ( M ... i ) |-> B )
27 26 nfrn
 |-  F/_ j ran ( j e. ( M ... i ) |-> B )
28 nfcv
 |-  F/_ j RR
29 nfcv
 |-  F/_ j <
30 27 28 29 nfsup
 |-  F/_ j sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < )
31 nfcv
 |-  F/_ j <_
32 nfcv
 |-  F/_ j y
33 30 31 32 nfbr
 |-  F/ j sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) <_ y
34 33 32 30 nfif
 |-  F/_ j if ( sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) <_ y , y , sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) )
35 2 ad3antrrr
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> M e. ZZ )
36 simpllr
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> y e. RR )
37 eqid
 |-  sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) = sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < )
38 eqid
 |-  if ( sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) <_ y , y , sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) ) = if ( sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) <_ y , y , sup ( ran ( j e. ( M ... i ) |-> B ) , RR , < ) )
39 simplr
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> i e. Z )
40 4 ad5ant15
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) /\ j e. Z ) -> B e. RR )
41 simpr
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> A. j e. ( ZZ>= ` i ) B <_ y )
42 25 34 35 3 36 37 38 39 40 41 uzublem
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> E. w e. RR A. j e. Z B <_ w )
43 42 rexlimdva2
 |-  ( ( ph /\ y e. RR ) -> ( E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y -> E. w e. RR A. j e. Z B <_ w ) )
44 43 imp
 |-  ( ( ( ph /\ y e. RR ) /\ E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y ) -> E. w e. RR A. j e. Z B <_ w )
45 44 rexlimdva2
 |-  ( ph -> ( E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y -> E. w e. RR A. j e. Z B <_ w ) )
46 45 imp
 |-  ( ( ph /\ E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y ) -> E. w e. RR A. j e. Z B <_ w )
47 19 46 sylan2
 |-  ( ( ph /\ E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) -> E. w e. RR A. j e. Z B <_ w )
48 47 ex
 |-  ( ph -> ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w -> E. w e. RR A. j e. Z B <_ w ) )
49 2 3 uzidd2
 |-  ( ph -> M e. Z )
50 49 ad2antrr
 |-  ( ( ( ph /\ w e. RR ) /\ A. j e. Z B <_ w ) -> M e. Z )
51 3 raleqi
 |-  ( A. j e. Z B <_ w <-> A. j e. ( ZZ>= ` M ) B <_ w )
52 51 biimpi
 |-  ( A. j e. Z B <_ w -> A. j e. ( ZZ>= ` M ) B <_ w )
53 52 adantl
 |-  ( ( ( ph /\ w e. RR ) /\ A. j e. Z B <_ w ) -> A. j e. ( ZZ>= ` M ) B <_ w )
54 nfv
 |-  F/ i A. j e. ( ZZ>= ` M ) B <_ w
55 fveq2
 |-  ( i = M -> ( ZZ>= ` i ) = ( ZZ>= ` M ) )
56 55 raleqdv
 |-  ( i = M -> ( A. j e. ( ZZ>= ` i ) B <_ w <-> A. j e. ( ZZ>= ` M ) B <_ w ) )
57 54 56 rspce
 |-  ( ( M e. Z /\ A. j e. ( ZZ>= ` M ) B <_ w ) -> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w )
58 50 53 57 syl2anc
 |-  ( ( ( ph /\ w e. RR ) /\ A. j e. Z B <_ w ) -> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w )
59 58 ex
 |-  ( ( ph /\ w e. RR ) -> ( A. j e. Z B <_ w -> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
60 59 reximdva
 |-  ( ph -> ( E. w e. RR A. j e. Z B <_ w -> E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
61 48 60 impbid
 |-  ( ph -> ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w <-> E. w e. RR A. j e. Z B <_ w ) )
62 breq2
 |-  ( w = x -> ( B <_ w <-> B <_ x ) )
63 62 ralbidv
 |-  ( w = x -> ( A. j e. Z B <_ w <-> A. j e. Z B <_ x ) )
64 63 cbvrexvw
 |-  ( E. w e. RR A. j e. Z B <_ w <-> E. x e. RR A. j e. Z B <_ x )
65 64 a1i
 |-  ( ph -> ( E. w e. RR A. j e. Z B <_ w <-> E. x e. RR A. j e. Z B <_ x ) )
66 14 61 65 3bitrd
 |-  ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. x e. RR A. j e. Z B <_ x ) )