Metamath Proof Explorer

Theorem ormkglobd

Description: If all adjacent elements of a certain sequence are ordered according to a relation which is a total order on S, then any element is so related to anything to right of it (so-called "global monotonicity"). Deduction form. (Contributed by Ender Ting, 30-Apr-2025)

Ref Expression
Hypotheses ormkglobd.1 ⊢ ( 𝜑 → 𝑅 Or 𝑆 )
ormkglobd.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 )
ormkglobd.3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
Assertion ormkglobd ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 ormkglobd.1 ⊢ ( 𝜑 → 𝑅 Or 𝑆 )
2 ormkglobd.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 )
3 ormkglobd.3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
4 2a1 ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → 𝜑 ) ) )
5 4 imp ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) ) → ( 𝑘 < 𝑡 → 𝜑 ) )
6 2a1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑘 < 𝑡 → 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ) )
7 6 imp ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → 𝑘 ∈ ( 0 ..^ 𝑇 ) ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) ) → ( 𝑘 < 𝑡 → 𝑘 ∈ ( 0 ..^ 𝑇 ) ) )
9 5 8 jcad ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) ) → ( 𝑘 < 𝑡 → ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ) )
10 elfzoelz ⊢ ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → 𝑡 ∈ ℤ )
11 10 adantl ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 𝑡 ∈ ℤ )
12 11 a1d ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → 𝑡 ∈ ℤ ) )
13 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ℤ )
14 13 adantr ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 𝑘 ∈ ℤ )
15 zltp1le ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑡 ∈ ℤ ) → ( 𝑘 < 𝑡 ↔ ( 𝑘 + 1 ) ≤ 𝑡 ) )
16 14 11 15 syl2anc ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 ↔ ( 𝑘 + 1 ) ≤ 𝑡 ) )
17 16 biimpd ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → ( 𝑘 + 1 ) ≤ 𝑡 ) )
18 11 zred ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 𝑡 ∈ ℝ )
19 elfzoel2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑇 ∈ ℤ )
20 19 adantr ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 𝑇 ∈ ℤ )
21 20 zred ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 𝑇 ∈ ℝ )
22 1red ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 1 ∈ ℝ )
23 18 21 22 3jca ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑡 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) )
24 elfzop1le2 ⊢ ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑡 + 1 ) ≤ ( 𝑇 + 1 ) )
25 24 adantl ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑡 + 1 ) ≤ ( 𝑇 + 1 ) )
26 leadd1 ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑡 ≤ 𝑇 ↔ ( 𝑡 + 1 ) ≤ ( 𝑇 + 1 ) ) )
27 26 biimprd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑡 + 1 ) ≤ ( 𝑇 + 1 ) → 𝑡 ≤ 𝑇 ) )
28 23 25 27 sylc ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → 𝑡 ≤ 𝑇 )
29 28 a1d ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → 𝑡 ≤ 𝑇 ) )
30 12 17 29 3jcad ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) ) → ( 𝑘 < 𝑡 → ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) )
32 9 31 jcad ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) ) → ( 𝑘 < 𝑡 → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) ) )
33 32 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) ) ) )
34 fveq2 ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
35 34 breq2d ⊢ ( 𝑎 = ( 𝑘 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
36 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑏 ) )
37 36 breq2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) )
38 fveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
39 38 breq2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
40 fveq2 ⊢ ( 𝑎 = 𝑡 → ( 𝐵 ‘ 𝑎 ) = ( 𝐵 ‘ 𝑡 ) )
41 40 breq2d ⊢ ( 𝑎 = 𝑡 → ( ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑎 ) ↔ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )
42 3 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
43 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝜑 )
44 43 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑅 Or 𝑆 )
45 elfzofz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ( 0 ... 𝑇 ) )
46 fzval3 ⊢ ( 𝑇 ∈ ℤ → ( 0 ... 𝑇 ) = ( 0 ..^ ( 𝑇 + 1 ) ) )
47 19 46 syl ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 0 ... 𝑇 ) = ( 0 ..^ ( 𝑇 + 1 ) ) )
48 45 47 eleqtrd ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) )
49 2 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 )
50 48 49 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 )
51 50 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 )
52 simp21 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ℤ )
53 0red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 0 ∈ ℝ )
54 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑘 ∈ ( 0 ..^ 𝑇 ) )
55 54 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑘 ∈ ℤ )
56 55 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑘 ∈ ℝ )
57 1red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 1 ∈ ℝ )
58 56 57 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
59 52 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ℝ )
60 elfzole1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 0 ≤ 𝑘 )
61 54 60 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 0 ≤ 𝑘 )
62 0le1 ⊢ 0 ≤ 1
63 62 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 0 ≤ 1 )
64 56 57 61 63 addge0d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 0 ≤ ( 𝑘 + 1 ) )
65 simp22 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑘 + 1 ) ≤ 𝑏 )
66 53 58 59 64 65 letrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 0 ≤ 𝑏 )
67 elnn0z ⊢ ( 𝑏 ∈ ℕ0 ↔ ( 𝑏 ∈ ℤ ∧ 0 ≤ 𝑏 ) )
68 52 66 67 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ℕ0 )
69 54 19 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑇 ∈ ℤ )
70 69 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑇 + 1 ) ∈ ℤ )
71 69 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑇 ∈ ℝ )
72 71 57 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑇 + 1 ) ∈ ℝ )
73 simp23 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 < 𝑇 )
74 71 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑇 < ( 𝑇 + 1 ) )
75 59 71 72 73 74 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 < ( 𝑇 + 1 ) )
76 elfzo0z ⊢ ( 𝑏 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ↔ ( 𝑏 ∈ ℕ0 ∧ ( 𝑇 + 1 ) ∈ ℤ ∧ 𝑏 < ( 𝑇 + 1 ) ) )
77 68 70 75 76 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) )
78 eleq1w ⊢ ( 𝑘 = 𝑏 → ( 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ↔ 𝑏 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) )
79 78 anbi2d ⊢ ( 𝑘 = 𝑏 → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) ↔ ( 𝜑 ∧ 𝑏 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) ) )
80 fveq2 ⊢ ( 𝑘 = 𝑏 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑏 ) )
81 80 eleq1d ⊢ ( 𝑘 = 𝑏 → ( ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 ↔ ( 𝐵 ‘ 𝑏 ) ∈ 𝑆 ) )
82 49 81 imbitrid ⊢ ( 𝑘 = 𝑏 → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ 𝑏 ) ∈ 𝑆 ) )
83 79 82 sylbird ⊢ ( 𝑘 = 𝑏 → ( ( 𝜑 ∧ 𝑏 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ 𝑏 ) ∈ 𝑆 ) )
84 ax6ev ⊢ ∃ 𝑘 𝑘 = 𝑏
85 83 84 exlimiiv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ 𝑏 ) ∈ 𝑆 )
86 43 77 85 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑏 ) ∈ 𝑆 )
87 1nn0 ⊢ 1 ∈ ℕ0
88 87 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 1 ∈ ℕ0 )
89 68 88 nn0addcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑏 + 1 ) ∈ ℕ0 )
90 59 71 57 73 ltadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑏 + 1 ) < ( 𝑇 + 1 ) )
91 elfzo0z ⊢ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ↔ ( ( 𝑏 + 1 ) ∈ ℕ0 ∧ ( 𝑇 + 1 ) ∈ ℤ ∧ ( 𝑏 + 1 ) < ( 𝑇 + 1 ) ) )
92 89 70 90 91 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝑏 + 1 ) ∈ ( 0 ..^ ( 𝑇 + 1 ) ) )
93 ovex ⊢ ( 𝑏 + 1 ) ∈ V
94 eleq1 ⊢ ( 𝑘 = ( 𝑏 + 1 ) → ( 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ↔ ( 𝑏 + 1 ) ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) )
95 94 anbi2d ⊢ ( 𝑘 = ( 𝑏 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) ↔ ( 𝜑 ∧ ( 𝑏 + 1 ) ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) ) )
96 fveq2 ⊢ ( 𝑘 = ( 𝑏 + 1 ) → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
97 96 eleq1d ⊢ ( 𝑘 = ( 𝑏 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 ↔ ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ 𝑆 ) )
98 49 97 imbitrid ⊢ ( 𝑘 = ( 𝑏 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ 𝑆 ) )
99 95 98 sylbird ⊢ ( 𝑘 = ( 𝑏 + 1 ) → ( ( 𝜑 ∧ ( 𝑏 + 1 ) ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ 𝑆 ) )
100 93 99 vtocle ⊢ ( ( 𝜑 ∧ ( 𝑏 + 1 ) ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ) → ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ 𝑆 )
101 43 92 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ ( 𝑏 + 1 ) ) ∈ 𝑆 )
102 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) )
103 elfzo0z ⊢ ( 𝑏 ∈ ( 0 ..^ 𝑇 ) ↔ ( 𝑏 ∈ ℕ0 ∧ 𝑇 ∈ ℤ ∧ 𝑏 < 𝑇 ) )
104 68 69 73 103 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → 𝑏 ∈ ( 0 ..^ 𝑇 ) )
105 eleq1w ⊢ ( 𝑏 = 𝑘 → ( 𝑏 ∈ ( 0 ..^ 𝑇 ) ↔ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) )
106 105 anbi2d ⊢ ( 𝑏 = 𝑘 → ( ( 𝜑 ∧ 𝑏 ∈ ( 0 ..^ 𝑇 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ) )
107 fveq2 ⊢ ( 𝑏 = 𝑘 → ( 𝐵 ‘ 𝑏 ) = ( 𝐵 ‘ 𝑘 ) )
108 fvoveq1 ⊢ ( 𝑏 = 𝑘 → ( 𝐵 ‘ ( 𝑏 + 1 ) ) = ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
109 107 108 breq12d ⊢ ( 𝑏 = 𝑘 → ( ( 𝐵 ‘ 𝑏 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) ↔ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
110 42 109 imbitrrid ⊢ ( 𝑏 = 𝑘 → ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝐵 ‘ 𝑏 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
111 106 110 sylbid ⊢ ( 𝑏 = 𝑘 → ( ( 𝜑 ∧ 𝑏 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝐵 ‘ 𝑏 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) ) )
112 ax6evr ⊢ ∃ 𝑘 𝑏 = 𝑘
113 111 112 exlimiiv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝐵 ‘ 𝑏 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
114 43 104 113 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑏 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
115 44 51 86 101 102 114 sotrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑏 ∧ 𝑏 < 𝑇 ) ∧ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑏 ) ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑏 + 1 ) ) )
116 13 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → 𝑘 ∈ ℤ )
117 116 peano2zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
118 19 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → 𝑇 ∈ ℤ )
119 elfzop1le2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ≤ 𝑇 )
120 119 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑘 + 1 ) ≤ 𝑇 )
121 35 37 39 41 42 115 117 118 120 fzindd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ ( 𝑡 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑡 ∧ 𝑡 ≤ 𝑇 ) ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) )
122 33 121 syl8 ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) ) )
123 122 ralrimivv ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )