Metamath Proof Explorer

Theorem lmcvg

Description: Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypotheses lmcvg.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
lmcvg.3 ⊢ ( 𝜑 → 𝑃 ∈ 𝑈 )
lmcvg.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
lmcvg.5 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
lmcvg.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
Assertion lmcvg ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 lmcvg.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 lmcvg.3 ⊢ ( 𝜑 → 𝑃 ∈ 𝑈 )
3 lmcvg.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 lmcvg.5 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
5 lmcvg.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
6 eleq2 ⊢ ( 𝑢 = 𝑈 → ( 𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑈 ) )
7 eleq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ 𝑈 ) )
8 7 rexralbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑈 ) )
9 6 8 imbi12d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑃 ∈ 𝑈 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑈 ) ) )
10 lmrcl ⊢ ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 → 𝐽 ∈ Top )
11 4 10 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
12 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
13 11 12 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
14 13 1 3 lmbr2 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) ∧ 𝑃 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
15 4 14 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝐽 ↑pm ℂ ) ∧ 𝑃 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
16 15 simp3d ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
17 simpr ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
18 17 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
19 18 reximi ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
20 19 imim2i ⊢ ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) → ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
21 20 ralimi ⊢ ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
22 16 21 syl ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
23 9 22 5 rspcdva ⊢ ( 𝜑 → ( 𝑃 ∈ 𝑈 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑈 ) )
24 2 23 mpd ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑈 )