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

Proof

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