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 |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝐵 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) ) |