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ℂ 𝐵 ) = ℂ )