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