# 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 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
climinff.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}$
climinff.3 ${⊢}{Z}={ℤ}_{\ge {M}}$
climinff.4 ${⊢}{\phi }\to {M}\in ℤ$
climinff.5 ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
climinff.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}+1\right)\le {F}\left({k}\right)$
climinff.7 ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)$
Assertion climinff ${⊢}{\phi }\to {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)$

### Proof

Step Hyp Ref Expression
1 climinff.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 climinff.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}$
3 climinff.3 ${⊢}{Z}={ℤ}_{\ge {M}}$
4 climinff.4 ${⊢}{\phi }\to {M}\in ℤ$
5 climinff.5 ${⊢}{\phi }\to {F}:{Z}⟶ℝ$
6 climinff.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}+1\right)\le {F}\left({k}\right)$
7 climinff.7 ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)$
8 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{j}\in {Z}$
9 1 8 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in {Z}\right)$
10 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({j}+1\right)$
11 2 10 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}\left({j}+1\right)$
12 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\le$
13 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{j}$
14 2 13 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)$
15 11 12 14 nfbr ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{F}\left({j}+1\right)\le {F}\left({j}\right)$
16 9 15 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}+1\right)\le {F}\left({j}\right)\right)$
17 eleq1w ${⊢}{k}={j}\to \left({k}\in {Z}↔{j}\in {Z}\right)$
18 17 anbi2d ${⊢}{k}={j}\to \left(\left({\phi }\wedge {k}\in {Z}\right)↔\left({\phi }\wedge {j}\in {Z}\right)\right)$
19 fvoveq1 ${⊢}{k}={j}\to {F}\left({k}+1\right)={F}\left({j}+1\right)$
20 fveq2 ${⊢}{k}={j}\to {F}\left({k}\right)={F}\left({j}\right)$
21 19 20 breq12d ${⊢}{k}={j}\to \left({F}\left({k}+1\right)\le {F}\left({k}\right)↔{F}\left({j}+1\right)\le {F}\left({j}\right)\right)$
22 18 21 imbi12d ${⊢}{k}={j}\to \left(\left(\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}+1\right)\le {F}\left({k}\right)\right)↔\left(\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}+1\right)\le {F}\left({j}\right)\right)\right)$
23 16 22 6 chvarfv ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to {F}\left({j}+1\right)\le {F}\left({j}\right)$
24 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℝ$
25 8 nfci ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{Z}$
26 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{x}$
27 26 12 14 nfbr ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)$
28 25 27 nfralw ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)$
29 24 28 nfrex ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)$
30 1 29 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\right)$
31 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)$
32 20 breq2d ${⊢}{k}={j}\to \left({x}\le {F}\left({k}\right)↔{x}\le {F}\left({j}\right)\right)$
33 31 27 32 cbvralw ${⊢}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)↔\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)$
34 33 a1i ${⊢}{k}={j}\to \left(\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)↔\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\right)$
35 34 rexbidv ${⊢}{k}={j}\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\right)$
36 35 imbi2d ${⊢}{k}={j}\to \left(\left({\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({k}\right)\right)↔\left({\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)\right)\right)$
37 30 36 7 chvarfv ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {F}\left({j}\right)$
38 3 4 5 23 37 climinf ${⊢}{\phi }\to {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)$