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	⊢ Ⅎ 𝑘 𝜑
	climinff.2	⊢ Ⅎ 𝑘 𝐹
	climinff.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climinff.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climinff.5	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	climinff.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
	climinff.7	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion	climinff	⊢ ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		climinff.1	⊢ Ⅎ 𝑘 𝜑
2		climinff.2	⊢ Ⅎ 𝑘 𝐹
3		climinff.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climinff.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climinff.5	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
6		climinff.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
7		climinff.7	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
8		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
9	1 8	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
10		nfcv	⊢ Ⅎ 𝑘 ( 𝑗 + 1 )
11	2 10	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) )
12		nfcv	⊢ Ⅎ 𝑘 ≤
13		nfcv	⊢ Ⅎ 𝑘 𝑗
14	2 13	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
15	11 12 14	nfbr	⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 )
16	9 15	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) )
17		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
18	17	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
19		fvoveq1	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
20		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
21	19 20	breq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) ) )
22	18 21	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
23	16 22 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) )
24		nfcv	⊢ Ⅎ 𝑘 ℝ
25	8	nfci	⊢ Ⅎ 𝑘 𝑍
26		nfcv	⊢ Ⅎ 𝑘 𝑥
27	26 12 14	nfbr	⊢ Ⅎ 𝑘 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
28	25 27	nfralw	⊢ Ⅎ 𝑘 ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
29	24 28	nfrexw	⊢ Ⅎ 𝑘 ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
30	1 29	nfim	⊢ Ⅎ 𝑘 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
31		nfv	⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
32	20	breq2d	⊢ ( 𝑘 = 𝑗 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
33	31 27 32	cbvralw	⊢ ( ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
34	33	a1i	⊢ ( 𝑘 = 𝑗 → ( ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
35	34	rexbidv	⊢ ( 𝑘 = 𝑗 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
36	35	imbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
37	30 36 7	chvarfv	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
38	3 4 5 23 37	climinf	⊢ ( 𝜑 → 𝐹 ⇝ inf ( ran 𝐹 , ℝ , < ) )