Metamath Proof Explorer

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 ffvelcdmda ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ 𝑋 )
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 ) )