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 biimpi ( ∀ 𝑗𝑍 𝐵𝑤 → ∀ 𝑗 ∈ ( ℤ𝑀 ) 𝐵𝑤 )
53 52 adantl ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑗𝑍 𝐵𝑤 ) → ∀ 𝑗 ∈ ( ℤ𝑀 ) 𝐵𝑤 )
54 nfv 𝑖𝑗 ∈ ( ℤ𝑀 ) 𝐵𝑤
55 fveq2 ( 𝑖 = 𝑀 → ( ℤ𝑖 ) = ( ℤ𝑀 ) )
56 55 raleqdv ( 𝑖 = 𝑀 → ( ∀ 𝑗 ∈ ( ℤ𝑖 ) 𝐵𝑤 ↔ ∀ 𝑗 ∈ ( ℤ𝑀 ) 𝐵𝑤 ) )
57 54 56 rspce ( ( 𝑀𝑍 ∧ ∀ 𝑗 ∈ ( ℤ𝑀 ) 𝐵𝑤 ) → ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝐵𝑤 )
58 50 53 57 syl2anc ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑗𝑍 𝐵𝑤 ) → ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝐵𝑤 )
59 58 ex ( ( 𝜑𝑤 ∈ ℝ ) → ( ∀ 𝑗𝑍 𝐵𝑤 → ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝐵𝑤 ) )
60 59 reximdva ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑤 → ∃ 𝑤 ∈ ℝ ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝐵𝑤 ) )
61 48 60 impbid ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝐵𝑤 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑤 ) )
62 breq2 ( 𝑤 = 𝑥 → ( 𝐵𝑤𝐵𝑥 ) )
63 62 ralbidv ( 𝑤 = 𝑥 → ( ∀ 𝑗𝑍 𝐵𝑤 ↔ ∀ 𝑗𝑍 𝐵𝑥 ) )
64 63 cbvrexvw ( ∃ 𝑤 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑤 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑥 )
65 64 a1i ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑤 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑥 ) )
66 14 61 65 3bitrd ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝐵𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 𝐵𝑥 ) )