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 ⊢ Ⅎ 𝑗 𝜑
uzub.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
uzub.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
uzub.12 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
Assertion uzub ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 uzub.1 ⊢ Ⅎ 𝑗 𝜑
2 uzub.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 uzub.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 uzub.12 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
5 fveq2 ⊢ ( 𝑘 = 𝑖 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑖 ) )
6 5 raleqdv ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑥 ) )
7 6 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑥 )
8 7 a1i ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑥 ) )
9 breq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐵 ≤ 𝑥 ↔ 𝐵 ≤ 𝑤 ) )
10 9 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) )
11 10 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) )
12 8 11 bitrd ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) )
13 12 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 )
14 13 a1i ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) )
15 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐵 ≤ 𝑤 ↔ 𝐵 ≤ 𝑦 ) )
16 15 ralbidv ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) )
17 16 rexbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) )
18 17 cbvrexvw ⊢ ( ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 )
19 18 biimpi ⊢ ( ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 → ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 )
20 nfv ⊢ Ⅎ 𝑗 𝑦 ∈ ℝ
21 1 20 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑦 ∈ ℝ )
22 nfv ⊢ Ⅎ 𝑗 𝑖 ∈ 𝑍
23 21 22 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 )
24 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦
25 23 24 nfan ⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 )
26 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 )
27 26 nfrn ⊢ Ⅎ 𝑗 ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 )
28 nfcv ⊢ Ⅎ 𝑗 ℝ
29 nfcv ⊢ Ⅎ 𝑗 <
30 27 28 29 nfsup ⊢ Ⅎ 𝑗 sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < )
31 nfcv ⊢ Ⅎ 𝑗 ≤
32 nfcv ⊢ Ⅎ 𝑗 𝑦
33 30 31 32 nfbr ⊢ Ⅎ 𝑗 sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ 𝑦
34 33 32 30 nfif ⊢ Ⅎ 𝑗 if ( sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
35 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → 𝑀 ∈ ℤ )
36 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
37 eqid ⊢ sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) = sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < )
38 eqid ⊢ if ( sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) = if ( sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) ↦ 𝐵 ) , ℝ , < ) )
39 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → 𝑖 ∈ 𝑍 )
40 4 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 )
42 25 34 35 3 36 37 38 39 40 41 uzublem ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 )
43 42 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) )
44 43 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 )
45 44 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) )
46 45 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 )
47 19 46 sylan2 ⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 )
48 47 ex ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 → ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) )
49 2 3 uzidd2 ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) → 𝑀 ∈ 𝑍 )
51 3 raleqi ⊢ ( ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) 𝐵 ≤ 𝑤 )
52 51 bilani ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) 𝐵 ≤ 𝑤 )
53 nfv ⊢ Ⅎ 𝑖 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) 𝐵 ≤ 𝑤
54 fveq2 ⊢ ( 𝑖 = 𝑀 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑀 ) )
55 54 raleqdv ⊢ ( 𝑖 = 𝑀 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) 𝐵 ≤ 𝑤 ) )
56 53 55 rspce ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) 𝐵 ≤ 𝑤 ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 )
57 50 52 56 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 )
58 57 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 → ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) )
59 58 reximdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 → ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ) )
60 48 59 impbid ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑤 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ) )
61 breq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐵 ≤ 𝑤 ↔ 𝐵 ≤ 𝑥 ) )
62 61 ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
63 62 cbvrexvw ⊢ ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )
64 63 a1i ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑤 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
65 14 60 64 3bitrd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )