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 ⊢ Ⅎ 𝑗 𝜑
uzublem.2 ⊢ Ⅎ 𝑗 𝑋
uzublem.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
uzublem.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
uzublem.5 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
uzublem.6 ⊢ 𝑊 = sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝐾 ) ↦ 𝐵 ) , ℝ , < )
uzublem.7 ⊢ 𝑋 = if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 )
uzublem.8 ⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
uzublem.9 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
uzublem.10 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝐵 ≤ 𝑌 )
Assertion uzublem ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )

Proof

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