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	$⊢ φ \to F : A ⟶ ℂ$
	limccl.a	$⊢ φ \to A \subseteq ℂ$
	limccl.b	$⊢ φ \to B \in ℂ$
	ellimc2.k	$⊢ K = TopOpen (ℂ_{fld})$
	limcnlp.n	$⊢ φ \to \neg B \in limPt (K) (A)$
Assertion	limcnlp	$⊢ φ \to F {lim}_{ℂ} B = ℂ$

Proof

Step	Hyp	Ref	Expression
1		limccl.f	$⊢ φ \to F : A ⟶ ℂ$
2		limccl.a	$⊢ φ \to A \subseteq ℂ$
3		limccl.b	$⊢ φ \to B \in ℂ$
4		ellimc2.k	$⊢ K = TopOpen (ℂ_{fld})$
5		limcnlp.n	$⊢ φ \to \neg B \in limPt (K) (A)$
6	1 2 3 4	ellimc2	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow (x \in ℂ \land \forall u \in K (x \in u \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))))$
7	4	cnfldtop	$⊢ K \in Top$
8	2	adantr	$⊢ (φ \land x \in ℂ) \to A \subseteq ℂ$
9	8	ssdifssd	$⊢ (φ \land x \in ℂ) \to A ∖ \{B\} \subseteq ℂ$
10	4	cnfldtopon	$⊢ K \in TopOn (ℂ)$
11	10	toponunii	$⊢ ℂ = ⋃ K$
12	11	clscld	$⊢ (K \in Top \land A ∖ \{B\} \subseteq ℂ) \to cls (K) (A ∖ \{B\}) \in Clsd (K)$
13	7 9 12	sylancr	$⊢ (φ \land x \in ℂ) \to cls (K) (A ∖ \{B\}) \in Clsd (K)$
14	11	cldopn	$⊢ cls (K) (A ∖ \{B\}) \in Clsd (K) \to ℂ ∖ cls (K) (A ∖ \{B\}) \in K$
15	13 14	syl	$⊢ (φ \land x \in ℂ) \to ℂ ∖ cls (K) (A ∖ \{B\}) \in K$
16	11	islp	$⊢ (K \in Top \land A \subseteq ℂ) \to (B \in limPt (K) (A) \leftrightarrow B \in cls (K) (A ∖ \{B\}))$
17	7 2 16	sylancr	$⊢ φ \to (B \in limPt (K) (A) \leftrightarrow B \in cls (K) (A ∖ \{B\}))$
18	5 17	mtbid	$⊢ φ \to \neg B \in cls (K) (A ∖ \{B\})$
19	3 18	eldifd	$⊢ φ \to B \in (ℂ ∖ cls (K) (A ∖ \{B\}))$
20	19	adantr	$⊢ (φ \land x \in ℂ) \to B \in (ℂ ∖ cls (K) (A ∖ \{B\}))$
21		difin2	$⊢ A ∖ \{B\} \subseteq ℂ \to (A ∖ \{B\}) ∖ cls (K) (A ∖ \{B\}) = (ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})$
22	9 21	syl	$⊢ (φ \land x \in ℂ) \to (A ∖ \{B\}) ∖ cls (K) (A ∖ \{B\}) = (ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})$
23	11	sscls	$⊢ (K \in Top \land A ∖ \{B\} \subseteq ℂ) \to A ∖ \{B\} \subseteq cls (K) (A ∖ \{B\})$
24	7 9 23	sylancr	$⊢ (φ \land x \in ℂ) \to A ∖ \{B\} \subseteq cls (K) (A ∖ \{B\})$
25		ssdif0	$⊢ A ∖ \{B\} \subseteq cls (K) (A ∖ \{B\}) \leftrightarrow (A ∖ \{B\}) ∖ cls (K) (A ∖ \{B\}) = \emptyset$
26	24 25	sylib	$⊢ (φ \land x \in ℂ) \to (A ∖ \{B\}) ∖ cls (K) (A ∖ \{B\}) = \emptyset$
27	22 26	eqtr3d	$⊢ (φ \land x \in ℂ) \to (ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\}) = \emptyset$
28	27	imaeq2d	$⊢ (φ \land x \in ℂ) \to F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})] = F [\emptyset]$
29		ima0	$⊢ F [\emptyset] = \emptyset$
30	28 29	eqtrdi	$⊢ (φ \land x \in ℂ) \to F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})] = \emptyset$
31		0ss	$⊢ \emptyset \subseteq u$
32	30 31	eqsstrdi	$⊢ (φ \land x \in ℂ) \to F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})] \subseteq u$
33		eleq2	$⊢ v = ℂ ∖ cls (K) (A ∖ \{B\}) \to (B \in v \leftrightarrow B \in (ℂ ∖ cls (K) (A ∖ \{B\})))$
34		ineq1	$⊢ v = ℂ ∖ cls (K) (A ∖ \{B\}) \to v \cap (A ∖ \{B\}) = (ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})$
35	34	imaeq2d	$⊢ v = ℂ ∖ cls (K) (A ∖ \{B\}) \to F [v \cap (A ∖ \{B\})] = F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})]$
36	35	sseq1d	$⊢ v = ℂ ∖ cls (K) (A ∖ \{B\}) \to (F [v \cap (A ∖ \{B\})] \subseteq u \leftrightarrow F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})] \subseteq u)$
37	33 36	anbi12d	$⊢ v = ℂ ∖ cls (K) (A ∖ \{B\}) \to ((B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow (B \in (ℂ ∖ cls (K) (A ∖ \{B\})) \land F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})] \subseteq u))$
38	37	rspcev	$⊢ (ℂ ∖ cls (K) (A ∖ \{B\}) \in K \land (B \in (ℂ ∖ cls (K) (A ∖ \{B\})) \land F [(ℂ ∖ cls (K) (A ∖ \{B\})) \cap (A ∖ \{B\})] \subseteq u)) \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)$
39	15 20 32 38	syl12anc	$⊢ (φ \land x \in ℂ) \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)$
40	39	a1d	$⊢ (φ \land x \in ℂ) \to (x \in u \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
41	40	ralrimivw	$⊢ (φ \land x \in ℂ) \to \forall u \in K (x \in u \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
42	41	ex	$⊢ φ \to (x \in ℂ \to \forall u \in K (x \in u \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
43	42	pm4.71d	$⊢ φ \to (x \in ℂ \leftrightarrow (x \in ℂ \land \forall u \in K (x \in u \to \exists v \in K (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))))$
44	6 43	bitr4d	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow x \in ℂ)$
45	44	eqrdv	$⊢ φ \to F {lim}_{ℂ} B = ℂ$

Metamath Proof Explorer

Theorem limcnlp

Proof