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

Metamath Proof Explorer

Theorem lmconst

Description: A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypothesis lmconst.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion lmconst ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 lmconst.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 simp2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑃 ∈ 𝑋 )
3 simp3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
4 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 3 4 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 5 1 eleqtrrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ 𝑍 )
7 idd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑃 ∈ 𝑢 → 𝑃 ∈ 𝑢 ) )
8 7 ralrimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∈ 𝑢 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) 𝑃 ∈ 𝑢 ) )
9 fveq2 ⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑀 ) )
10 9 raleqdv ⊢ ( 𝑗 = 𝑀 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) 𝑃 ∈ 𝑢 ) )
11 10 rspcev ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) 𝑃 ∈ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 )
12 6 8 11 syl6an ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) )
13 12 ralrimivw ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) )
14 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 fconst6g ⊢ ( 𝑃 ∈ 𝑋 → ( 𝑍 × { 𝑃 } ) : 𝑍 ⟶ 𝑋 )
16 2 15 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) : 𝑍 ⟶ 𝑋 )
17 fvconst2g ⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 𝑃 } ) ‘ 𝑘 ) = 𝑃 )
18 2 17 sylan ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 𝑃 } ) ‘ 𝑘 ) = 𝑃 )
19 14 1 3 16 18 lmbrf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑍 × { 𝑃 } ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) ) ) )
20 2 13 19 mpbir2and ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )