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\phi$$
	climinff.2	$$⊢\underset{\_}{Ⅎ}kF$$
	climinff.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climinff.4	$$⊢\phi \to M\in \mathbb{Z}$$
	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 ℝ\forall k\in Zx\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\phi$$
2		climinff.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		climinff.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		climinff.4	$$⊢\phi \to M\in \mathbb{Z}$$
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 ℝ\forall k\in Zx\le F\left(k\right)$$
8		nfv	$$⊢Ⅎkj\in Z$$
9	1 8	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(j+1\right)$$
11	2 10	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j+1\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
14	2 13	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
15	11 12 14	nfbr	$$⊢ℲkF\left(j+1\right)\le F\left(j\right)$$
16	9 15	nfim	$$⊢Ⅎk\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\leftrightarrow j\in Z\right)$$
18	17	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \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)\leftrightarrow 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)\leftrightarrow \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ℝ$$
25	8	nfci	$$⊢\underset{\_}{Ⅎ}kZ$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
27	26 12 14	nfbr	$$⊢Ⅎkx\le F\left(j\right)$$
28	25 27	nfralw	$$⊢Ⅎk\forall j\in Zx\le F\left(j\right)$$
29	24 28	nfrexw	$$⊢Ⅎk\exists x\in ℝ\forall j\in Zx\le F\left(j\right)$$
30	1 29	nfim	$$⊢Ⅎk\left(\phi \to \exists x\in ℝ\forall j\in Zx\le F\left(j\right)\right)$$
31		nfv	$$⊢Ⅎjx\le F\left(k\right)$$
32	20	breq2d	$$⊢k=j\to \left(x\le F\left(k\right)\leftrightarrow x\le F\left(j\right)\right)$$
33	31 27 32	cbvralw	$$⊢\forall k\in Zx\le F\left(k\right)\leftrightarrow \forall j\in Zx\le F\left(j\right)$$
34	33	a1i	$$⊢k=j\to \left(\forall k\in Zx\le F\left(k\right)\leftrightarrow \forall j\in Zx\le F\left(j\right)\right)$$
35	34	rexbidv	$$⊢k=j\to \left(\exists x\in ℝ\forall k\in Zx\le F\left(k\right)\leftrightarrow \exists x\in ℝ\forall j\in Zx\le F\left(j\right)\right)$$
36	35	imbi2d	$$⊢k=j\to \left(\left(\phi \to \exists x\in ℝ\forall k\in Zx\le F\left(k\right)\right)\leftrightarrow \left(\phi \to \exists x\in ℝ\forall j\in Zx\le F\left(j\right)\right)\right)$$
37	30 36 7	chvarfv	$$⊢\phi \to \exists x\in ℝ\forall j\in Zx\le F\left(j\right)$$
38	3 4 5 23 37	climinf	$$⊢\phi \to F⇝sup\left(\mathrm{ran}F,ℝ,<\right)$$