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

Metamath Proof Explorer

Theorem limcnlp

Description: If B is not a limit point of the domain of the function F , then every point is a limit of F at B . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limccl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limccl.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limccl.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
ellimc2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limcnlp.n ⊢ ( 𝜑 → ¬ 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
Assertion limcnlp ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ℂ )

Proof

Step Hyp Ref Expression
1 limccl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limccl.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 limccl.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4 ellimc2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 limcnlp.n ⊢ ( 𝜑 → ¬ 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
6 1 2 3 4 ellimc2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )
7 4 cnfldtop ⊢ 𝐾 ∈ Top
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐴 ⊆ ℂ )
9 8 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
10 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
11 10 toponunii ⊢ ℂ = ∪ 𝐾
12 11 clscld ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ∈ ( Clsd ‘ 𝐾 ) )
13 7 9 12 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ∈ ( Clsd ‘ 𝐾 ) )
14 11 cldopn ⊢ ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ∈ ( Clsd ‘ 𝐾 ) → ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∈ 𝐾 )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∈ 𝐾 )
16 11 islp ⊢ ( ( 𝐾 ∈ Top ∧ 𝐴 ⊆ ℂ ) → ( 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
17 7 2 16 sylancr ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
18 5 17 mtbid ⊢ ( 𝜑 → ¬ 𝐵 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
19 3 18 eldifd ⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
21 difin2 ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ → ( ( 𝐴 ∖ { 𝐵 } ) ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) = ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
22 9 21 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ∖ { 𝐵 } ) ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) = ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
23 11 sscls ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
24 7 9 23 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
25 ssdif0 ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ( ( 𝐴 ∖ { 𝐵 } ) ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) = ∅ )
26 24 25 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ∖ { 𝐵 } ) ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) = ∅ )
27 22 26 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ )
28 27 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) = ( 𝐹 “ ∅ ) )
29 ima0 ⊢ ( 𝐹 “ ∅ ) = ∅
30 28 29 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) = ∅ )
31 0ss ⊢ ∅ ⊆ 𝑢
32 30 31 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 )
33 eleq2 ⊢ ( 𝑣 = ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) → ( 𝐵 ∈ 𝑣 ↔ 𝐵 ∈ ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ) )
34 ineq1 ⊢ ( 𝑣 = ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) → ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
35 34 imaeq2d ⊢ ( 𝑣 = ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) → ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) = ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) )
36 35 sseq1d ⊢ ( 𝑣 = ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) → ( ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
37 33 36 anbi12d ⊢ ( 𝑣 = ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) → ( ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐵 ∈ ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∧ ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
38 37 rspcev ⊢ ( ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∈ 𝐾 ∧ ( 𝐵 ∈ ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∧ ( 𝐹 “ ( ( ℂ ∖ ( ( cls ‘ 𝐾 ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
39 15 20 32 38 syl12anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
40 39 a1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ∈ 𝑢 → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
41 40 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
42 41 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ → ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
43 42 pm4.71d ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑣 ∈ 𝐾 ( 𝐵 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )
44 6 43 bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ℂ ) )
45 44 eqrdv ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ℂ )