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 
|- ( ph -> R Or S )
ormklocald.2 
|- ( ph -> A. k e. ( 0 ..^ ( T + 1 ) ) ( B ` k ) e. S )
ormklocald.3 
|- ( ph -> A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) R ( B ` t ) ) )
Assertion ormklocald 
|- ( ph -> A. k e. ( 0 ..^ T ) ( B ` k ) R ( B ` ( k + 1 ) ) )

Proof

Step Hyp Ref Expression
1 ormklocald.1 
 |-  ( ph -> R Or S )
2 ormklocald.2 
 |-  ( ph -> A. k e. ( 0 ..^ ( T + 1 ) ) ( B ` k ) e. S )
3 ormklocald.3 
 |-  ( ph -> A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) R ( B ` t ) ) )
4 ovex 
 |-  ( k + 1 ) e. _V
5 4 isseti 
 |-  E. t t = ( k + 1 )
6 elfzoelz 
 |-  ( k e. ( 0 ..^ T ) -> k e. ZZ )
7 6 zred 
 |-  ( k e. ( 0 ..^ T ) -> k e. RR )
8 7 ltp1d 
 |-  ( k e. ( 0 ..^ T ) -> k < ( k + 1 ) )
9 breq2 
 |-  ( t = ( k + 1 ) -> ( k < t <-> k < ( k + 1 ) ) )
10 8 9 syl5ibrcom 
 |-  ( k e. ( 0 ..^ T ) -> ( t = ( k + 1 ) -> k < t ) )
11 10 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( t = ( k + 1 ) -> k < t ) )
12 1z 
 |-  1 e. ZZ
13 fzoaddel 
 |-  ( ( k e. ( 0 ..^ T ) /\ 1 e. ZZ ) -> ( k + 1 ) e. ( ( 0 + 1 ) ..^ ( T + 1 ) ) )
14 12 13 mpan2 
 |-  ( k e. ( 0 ..^ T ) -> ( k + 1 ) e. ( ( 0 + 1 ) ..^ ( T + 1 ) ) )
15 0p1e1 
 |-  ( 0 + 1 ) = 1
16 15 oveq1i 
 |-  ( ( 0 + 1 ) ..^ ( T + 1 ) ) = ( 1 ..^ ( T + 1 ) )
17 14 16 eleqtrdi 
 |-  ( k e. ( 0 ..^ T ) -> ( k + 1 ) e. ( 1 ..^ ( T + 1 ) ) )
18 eleq1 
 |-  ( t = ( k + 1 ) -> ( t e. ( 1 ..^ ( T + 1 ) ) <-> ( k + 1 ) e. ( 1 ..^ ( T + 1 ) ) ) )
19 17 18 syl5ibrcom 
 |-  ( k e. ( 0 ..^ T ) -> ( t = ( k + 1 ) -> t e. ( 1 ..^ ( T + 1 ) ) ) )
20 19 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( t = ( k + 1 ) -> t e. ( 1 ..^ ( T + 1 ) ) ) )
21 3 r19.21bi 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> A. t e. ( 1 ..^ ( T + 1 ) ) ( k < t -> ( B ` k ) R ( B ` t ) ) )
22 21 r19.21bi 
 |-  ( ( ( ph /\ k e. ( 0 ..^ T ) ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) -> ( k < t -> ( B ` k ) R ( B ` t ) ) )
23 22 ex 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( t e. ( 1 ..^ ( T + 1 ) ) -> ( k < t -> ( B ` k ) R ( B ` t ) ) ) )
24 20 23 syld 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( t = ( k + 1 ) -> ( k < t -> ( B ` k ) R ( B ` t ) ) ) )
25 11 24 mpdd 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( t = ( k + 1 ) -> ( B ` k ) R ( B ` t ) ) )
26 fveq2 
 |-  ( t = ( k + 1 ) -> ( B ` t ) = ( B ` ( k + 1 ) ) )
27 26 breq2d 
 |-  ( t = ( k + 1 ) -> ( ( B ` k ) R ( B ` t ) <-> ( B ` k ) R ( B ` ( k + 1 ) ) ) )
28 25 27 mpbidi 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( t = ( k + 1 ) -> ( B ` k ) R ( B ` ( k + 1 ) ) ) )
29 28 eximdv 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( E. t t = ( k + 1 ) -> E. t ( B ` k ) R ( B ` ( k + 1 ) ) ) )
30 5 29 mpi 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> E. t ( B ` k ) R ( B ` ( k + 1 ) ) )
31 ax5e 
 |-  ( E. t ( B ` k ) R ( B ` ( k + 1 ) ) -> ( B ` k ) R ( B ` ( k + 1 ) ) )
32 30 31 syl 
 |-  ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( B ` k ) R ( B ` ( k + 1 ) ) )
33 32 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ..^ T ) ( B ` k ) R ( B ` ( k + 1 ) ) )