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