Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | monoordxr.p | |
|
monoordxr.k | |
||
monoordxr.n | |
||
monoordxr.x | |
||
monoordxr.l | |
||
Assertion | monoordxr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | monoordxr.p | |
|
2 | monoordxr.k | |
|
3 | monoordxr.n | |
|
4 | monoordxr.x | |
|
5 | monoordxr.l | |
|
6 | nfv | |
|
7 | 1 6 | nfan | |
8 | nfcv | |
|
9 | 2 8 | nffv | |
10 | nfcv | |
|
11 | 9 10 | nfel | |
12 | 7 11 | nfim | |
13 | eleq1w | |
|
14 | 13 | anbi2d | |
15 | fveq2 | |
|
16 | 15 | eleq1d | |
17 | 14 16 | imbi12d | |
18 | 12 17 4 | chvarfv | |
19 | nfv | |
|
20 | 1 19 | nfan | |
21 | nfcv | |
|
22 | nfcv | |
|
23 | 2 22 | nffv | |
24 | 9 21 23 | nfbr | |
25 | 20 24 | nfim | |
26 | eleq1w | |
|
27 | 26 | anbi2d | |
28 | fvoveq1 | |
|
29 | 15 28 | breq12d | |
30 | 27 29 | imbi12d | |
31 | 25 30 5 | chvarfv | |
32 | 3 18 31 | monoordxrv | |