This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑘 𝜑
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 𝐹 , ℝ , < ) )