Metamath Proof Explorer

Theorem ormklocald

Description: If elements of a certain sequence are ordered with respect to a certain relation, then its consecutive elements satisfy that relation (so-called "local monotonicity"). (Contributed by Ender Ting, 30-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 ormklocald.1 ⊢ ( 𝜑 → 𝑅 Or 𝑆 )
2 ormklocald.2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ( 𝐵 ‘ 𝑘 ) ∈ 𝑆 )
3 ormklocald.3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )
4 ovex ⊢ ( 𝑘 + 1 ) ∈ V
5 4 isseti ⊢ ∃ 𝑡 𝑡 = ( 𝑘 + 1 )
6 elfzoelz ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ℤ )
7 6 zred ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 ∈ ℝ )
8 7 ltp1d ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → 𝑘 < ( 𝑘 + 1 ) )
9 breq2 ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 ↔ 𝑘 < ( 𝑘 + 1 ) ) )
10 8 9 syl5ibrcom ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 = ( 𝑘 + 1 ) → 𝑘 < 𝑡 ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑡 = ( 𝑘 + 1 ) → 𝑘 < 𝑡 ) )
12 1z ⊢ 1 ∈ ℤ
13 fzoaddel ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑇 ) ∧ 1 ∈ ℤ ) → ( 𝑘 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑇 + 1 ) ) )
14 12 13 mpan2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( 𝑇 + 1 ) ) )
15 0p1e1 ⊢ ( 0 + 1 ) = 1
16 15 oveq1i ⊢ ( ( 0 + 1 ) ..^ ( 𝑇 + 1 ) ) = ( 1 ..^ ( 𝑇 + 1 ) )
17 14 16 eleqtrdi ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑘 + 1 ) ∈ ( 1 ..^ ( 𝑇 + 1 ) ) )
18 eleq1 ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) )
19 17 18 syl5ibrcom ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑇 ) → ( 𝑡 = ( 𝑘 + 1 ) → 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑡 = ( 𝑘 + 1 ) → 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) )
21 3 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ∀ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )
22 21 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) ∧ 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )
23 22 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑡 ∈ ( 1 ..^ ( 𝑇 + 1 ) ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) ) )
24 20 23 syld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝑘 < 𝑡 → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) ) )
25 11 24 mpdd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ) )
26 fveq2 ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑡 ) = ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
27 26 breq2d ⊢ ( 𝑡 = ( 𝑘 + 1 ) → ( ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ 𝑡 ) ↔ ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
28 25 27 mpbidi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝑡 = ( 𝑘 + 1 ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
29 28 eximdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( ∃ 𝑡 𝑡 = ( 𝑘 + 1 ) → ∃ 𝑡 ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) ) )
30 5 29 mpi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ∃ 𝑡 ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
31 ax5e ⊢ ( ∃ 𝑡 ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑇 ) ) → ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑇 ) ( 𝐵 ‘ 𝑘 ) 𝑅 ( 𝐵 ‘ ( 𝑘 + 1 ) ) )