Metamath Proof Explorer


Theorem uzublem

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 uzublem.1 j φ
uzublem.2 _ j X
uzublem.3 φ M
uzublem.4 Z = M
uzublem.5 φ Y
uzublem.6 W = sup ran j M K B <
uzublem.7 X = if W Y Y W
uzublem.8 φ K Z
uzublem.9 φ j Z B
uzublem.10 φ j K B Y
Assertion uzublem φ x j Z B x

Proof

Step Hyp Ref Expression
1 uzublem.1 j φ
2 uzublem.2 _ j X
3 uzublem.3 φ M
4 uzublem.4 Z = M
5 uzublem.5 φ Y
6 uzublem.6 W = sup ran j M K B <
7 uzublem.7 X = if W Y Y W
8 uzublem.8 φ K Z
9 uzublem.9 φ j Z B
10 uzublem.10 φ j K B Y
11 6 a1i φ W = sup ran j M K B <
12 ltso < Or
13 12 a1i φ < Or
14 fzfid φ M K Fin
15 4 eluzelz2 K Z K
16 8 15 syl φ K
17 3 zred φ M
18 17 leidd φ M M
19 8 4 eleqtrdi φ K M
20 eluzle K M M K
21 19 20 syl φ M K
22 3 16 3 18 21 elfzd φ M M K
23 22 ne0d φ M K
24 fzssuz M K M
25 4 eqcomi M = Z
26 24 25 sseqtri M K Z
27 id j M K j M K
28 26 27 sseldi j M K j Z
29 28 9 sylan2 φ j M K B
30 1 13 14 23 29 fisupclrnmpt φ sup ran j M K B <
31 11 30 eqeltrd φ W
32 5 31 ifcld φ if W Y Y W
33 7 32 eqeltrid φ X
34 9 adantr φ j Z K j B
35 5 ad2antrr φ j Z K j Y
36 33 ad2antrr φ j Z K j X
37 10 ad2antrr φ j Z K j j K B Y
38 eqid K = K
39 16 ad2antrr φ j Z K j K
40 4 eluzelz2 j Z j
41 40 ad2antlr φ j Z K j j
42 simpr φ j Z K j K j
43 38 39 41 42 eluzd φ j Z K j j K
44 rspa j K B Y j K B Y
45 37 43 44 syl2anc φ j Z K j B Y
46 max2 W Y Y if W Y Y W
47 31 5 46 syl2anc φ Y if W Y Y W
48 47 7 breqtrrdi φ Y X
49 48 ad2antrr φ j Z K j Y X
50 34 35 36 45 49 letrd φ j Z K j B X
51 simpr φ j Z ¬ K j ¬ K j
52 uzssre M
53 4 52 eqsstri Z
54 53 sseli j Z j
55 54 ad2antlr φ j Z ¬ K j j
56 53 8 sseldi φ K
57 56 ad2antrr φ j Z ¬ K j K
58 55 57 ltnled φ j Z ¬ K j j < K ¬ K j
59 51 58 mpbird φ j Z ¬ K j j < K
60 9 adantr φ j Z j < K B
61 6 31 eqeltrrid φ sup ran j M K B <
62 6 61 eqeltrid φ W
63 62 ad2antrr φ j Z j < K W
64 5 62 ifcld φ if W Y Y W
65 7 64 eqeltrid φ X
66 65 ad2antrr φ j Z j < K X
67 simpll φ j Z j < K φ
68 3 ad2antrr φ j Z j < K M
69 16 ad2antrr φ j Z j < K K
70 4 eleq2i j Z j M
71 70 biimpi j Z j M
72 71 ad2antlr φ j Z j < K j M
73 simpr φ j Z j < K j < K
74 72 69 73 elfzod φ j Z j < K j M ..^ K
75 elfzouz j M ..^ K j M
76 75 25 eleqtrdi j M ..^ K j Z
77 74 76 40 3syl φ j Z j < K j
78 eluzle j M M j
79 71 78 syl j Z M j
80 79 ad2antlr φ j Z j < K M j
81 74 76 54 3syl φ j Z j < K j
82 56 ad2antrr φ j Z j < K K
83 81 82 73 ltled φ j Z j < K j K
84 68 69 77 80 83 elfzd φ j Z j < K j M K
85 1 29 ralrimia φ j M K B
86 fimaxre3 M K Fin j M K B y j M K B y
87 14 85 86 syl2anc φ y j M K B y
88 1 29 87 suprubrnmpt φ j M K B sup ran j M K B <
89 67 84 88 syl2anc φ j Z j < K B sup ran j M K B <
90 89 6 breqtrrdi φ j Z j < K B W
91 max1 W Y W if W Y Y W
92 31 5 91 syl2anc φ W if W Y Y W
93 92 7 breqtrrdi φ W X
94 93 ad2antrr φ j Z j < K W X
95 60 63 66 90 94 letrd φ j Z j < K B X
96 59 95 syldan φ j Z ¬ K j B X
97 50 96 pm2.61dan φ j Z B X
98 97 ex φ j Z B X
99 1 98 ralrimi φ j Z B X
100 nfv x j Z B X
101 nfcv _ j x
102 101 2 nfeq j x = X
103 breq2 x = X B x B X
104 102 103 ralbid x = X j Z B x j Z B X
105 100 104 rspce X j Z B X x j Z B x
106 33 99 105 syl2anc φ x j Z B x