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 ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )