Metamath Proof Explorer

Theorem climinff

Description: A version of climinf using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 15-Sep-2020)

Ref Expression
Hypotheses climinff.1 
|- F/ k ph
climinff.2 
|- F/_ k F
climinff.3 
|- Z = ( ZZ>= ` M )
climinff.4 
|- ( ph -> M e. ZZ )
climinff.5 
|- ( ph -> F : Z --> RR )
climinff.6 
|- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
climinff.7 
|- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )
Assertion climinff 
|- ( ph -> F ~~> inf ( ran F , RR , < ) )

Proof

Step Hyp Ref Expression
1 climinff.1 
 |-  F/ k ph
2 climinff.2 
 |-  F/_ k F
3 climinff.3 
 |-  Z = ( ZZ>= ` M )
4 climinff.4 
 |-  ( ph -> M e. ZZ )
5 climinff.5 
 |-  ( ph -> F : Z --> RR )
6 climinff.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
7 climinff.7 
 |-  ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )
8 nfv 
 |-  F/ k j e. Z
9 1 8 nfan 
 |-  F/ k ( ph /\ j e. Z )
10 nfcv 
 |-  F/_ k ( j + 1 )
11 2 10 nffv 
 |-  F/_ k ( F ` ( j + 1 ) )
12 nfcv 
 |-  F/_ k <_
13 nfcv 
 |-  F/_ k j
14 2 13 nffv 
 |-  F/_ k ( F ` j )
15 11 12 14 nfbr 
 |-  F/ k ( F ` ( j + 1 ) ) <_ ( F ` j )
16 9 15 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( F ` ( j + 1 ) ) <_ ( F ` j ) )
17 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
18 17 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
19 fvoveq1 
 |-  ( k = j -> ( F ` ( k + 1 ) ) = ( F ` ( j + 1 ) ) )
20 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
21 19 20 breq12d 
 |-  ( k = j -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) <-> ( F ` ( j + 1 ) ) <_ ( F ` j ) ) )
22 18 21 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) ) <-> ( ( ph /\ j e. Z ) -> ( F ` ( j + 1 ) ) <_ ( F ` j ) ) ) )
23 16 22 6 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( F ` ( j + 1 ) ) <_ ( F ` j ) )
24 nfcv 
 |-  F/_ k RR
25 8 nfci 
 |-  F/_ k Z
26 nfcv 
 |-  F/_ k x
27 26 12 14 nfbr 
 |-  F/ k x <_ ( F ` j )
28 25 27 nfralw 
 |-  F/ k A. j e. Z x <_ ( F ` j )
29 24 28 nfrex 
 |-  F/ k E. x e. RR A. j e. Z x <_ ( F ` j )
30 1 29 nfim 
 |-  F/ k ( ph -> E. x e. RR A. j e. Z x <_ ( F ` j ) )
31 nfv 
 |-  F/ j x <_ ( F ` k )
32 20 breq2d 
 |-  ( k = j -> ( x <_ ( F ` k ) <-> x <_ ( F ` j ) ) )
33 31 27 32 cbvralw 
 |-  ( A. k e. Z x <_ ( F ` k ) <-> A. j e. Z x <_ ( F ` j ) )
34 33 a1i 
 |-  ( k = j -> ( A. k e. Z x <_ ( F ` k ) <-> A. j e. Z x <_ ( F ` j ) ) )
35 34 rexbidv 
 |-  ( k = j -> ( E. x e. RR A. k e. Z x <_ ( F ` k ) <-> E. x e. RR A. j e. Z x <_ ( F ` j ) ) )
36 35 imbi2d 
 |-  ( k = j -> ( ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) ) <-> ( ph -> E. x e. RR A. j e. Z x <_ ( F ` j ) ) ) )
37 30 36 7 chvarfv 
 |-  ( ph -> E. x e. RR A. j e. Z x <_ ( F ` j ) )
38 3 4 5 23 37 climinf 
 |-  ( ph -> F ~~> inf ( ran F , RR , < ) )