Theorem lmclim2

Description: A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	lmclim2.2	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
	lmclim2.3	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
	lmclim2.4	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	lmclim2.5	⊢ 𝐺 = ( 𝑥 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐷 𝑌 ) )
	lmclim2.6	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
Assertion	lmclim2	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑌 ↔ 𝐺 ⇝ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lmclim2.2	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
2		lmclim2.3	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
3		lmclim2.4	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
4		lmclim2.5	⊢ 𝐺 = ( 𝑥 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐷 𝑌 ) )
5		lmclim2.6	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
6		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7	1 6	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
9		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
10		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
11	3 7 8 9 10 2	lmmbrf	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑌 ↔ ( 𝑌 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) ) )
12		nnex	⊢ ℕ ∈ V
13	12	mptex	⊢ ( 𝑥 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐷 𝑌 ) ) ∈ V
14	4 13	eqeltri	⊢ 𝐺 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝐺 ∈ V )
16		fveq2	⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
17	16	oveq1d	⊢ ( 𝑥 = 𝑘 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 𝑌 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) )
18		ovex	⊢ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ∈ V
19	17 4 18	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) )
21	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
22	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
23	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑌 ∈ 𝑋 )
24		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ∈ ℝ )
25	21 22 23 24	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ∈ ℝ )
26	25	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ∈ ℂ )
27	8 9 15 20 26	clim0c	⊢ ( 𝜑 → ( 𝐺 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ) )
28		eluznn	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
29		metge0	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) → 0 ≤ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) )
30	21 22 23 29	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) )
31	25 30	absidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) )
32	31	breq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) )
33	28 32	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) )
34	33	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) )
35	34	ralbidva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) )
36	35	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) )
37	36	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) )
38	5	biantrurd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ↔ ( 𝑌 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) ) )
39	27 37 38	3bitrrd	⊢ ( 𝜑 → ( ( 𝑌 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑌 ) < 𝑥 ) ↔ 𝐺 ⇝ 0 ) )
40	11 39	bitrd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑌 ↔ 𝐺 ⇝ 0 ) )