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 j φ
uzub.2 φ M
uzub.3 Z = M
uzub.12 φ j Z B
Assertion uzub φ x k Z j k B x x j Z B x

Proof

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