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