Metamath Proof Explorer


Theorem monoordxr

Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022)

Ref Expression
Hypotheses monoordxr.p kφ
monoordxr.k _kF
monoordxr.n φNM
monoordxr.x φkMNFk*
monoordxr.l φkMN1FkFk+1
Assertion monoordxr φFMFN

Proof

Step Hyp Ref Expression
1 monoordxr.p kφ
2 monoordxr.k _kF
3 monoordxr.n φNM
4 monoordxr.x φkMNFk*
5 monoordxr.l φkMN1FkFk+1
6 nfv kjMN
7 1 6 nfan kφjMN
8 nfcv _kj
9 2 8 nffv _kFj
10 nfcv _k*
11 9 10 nfel kFj*
12 7 11 nfim kφjMNFj*
13 eleq1w k=jkMNjMN
14 13 anbi2d k=jφkMNφjMN
15 fveq2 k=jFk=Fj
16 15 eleq1d k=jFk*Fj*
17 14 16 imbi12d k=jφkMNFk*φjMNFj*
18 12 17 4 chvarfv φjMNFj*
19 nfv kjMN1
20 1 19 nfan kφjMN1
21 nfcv _k
22 nfcv _kj+1
23 2 22 nffv _kFj+1
24 9 21 23 nfbr kFjFj+1
25 20 24 nfim kφjMN1FjFj+1
26 eleq1w k=jkMN1jMN1
27 26 anbi2d k=jφkMN1φjMN1
28 fvoveq1 k=jFk+1=Fj+1
29 15 28 breq12d k=jFkFk+1FjFj+1
30 27 29 imbi12d k=jφkMN1FkFk+1φjMN1FjFj+1
31 25 30 5 chvarfv φjMN1FjFj+1
32 3 18 31 monoordxrv φFMFN