Metamath Proof Explorer

Theorem lmlim

Description: Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on CC on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses lmlim.j ⊢ 𝐽 ∈ ( TopOn ‘ 𝑌 )
lmlim.f ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
lmlim.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
lmlim.t ⊢ ( 𝐽 ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 )
lmlim.x ⊢ 𝑋 ⊆ ℂ
Assertion lmlim ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 lmlim.j ⊢ 𝐽 ∈ ( TopOn ‘ 𝑌 )
2 lmlim.f ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
3 lmlim.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
4 lmlim.t ⊢ ( 𝐽 ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 )
5 lmlim.x ⊢ 𝑋 ⊆ ℂ
6 eqid ⊢ ( 𝐽 ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 )
7 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
8 cnex ⊢ ℂ ∈ V
9 8 a1i ⊢ ( 𝜑 → ℂ ∈ V )
10 5 a1i ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
11 9 10 ssexd ⊢ ( 𝜑 → 𝑋 ∈ V )
12 1 topontopi ⊢ 𝐽 ∈ Top
13 12 a1i ⊢ ( 𝜑 → 𝐽 ∈ Top )
14 1z ⊢ 1 ∈ ℤ
15 14 a1i ⊢ ( 𝜑 → 1 ∈ ℤ )
16 6 7 11 13 3 15 2 lmss ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑋 ) ) 𝑃 ) )
17 4 fveq2i ⊢ ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑋 ) ) = ( ⇝𝑡 ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) )
18 17 breqi ⊢ ( 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑋 ) ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) 𝑃 )
19 18 a1i ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑋 ) ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) 𝑃 ) )
20 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 )
21 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
22 21 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
23 22 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
24 20 7 11 23 3 15 2 lmss ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) 𝑃 ) )
25 fss ⊢ ( ( 𝐹 : ℕ ⟶ 𝑋 ∧ 𝑋 ⊆ ℂ ) → 𝐹 : ℕ ⟶ ℂ )
26 2 5 25 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
27 21 7 lmclimf ⊢ ( ( 1 ∈ ℤ ∧ 𝐹 : ℕ ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )
28 14 26 27 sylancr ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )
29 24 28 bitr3d ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )
30 16 19 29 3bitrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )