limcflf

Description: The limit operator can be expressed as a filter limit, from the filter of neighborhoods of B restricted to A \ { B } , to the topology of the complex numbers. (If B is not a limit point of A , then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	limcflf.f	$⊢ φ \to F : A ⟶ ℂ$
	limcflf.a	$⊢ φ \to A \subseteq ℂ$
	limcflf.b	$⊢ φ \to B \in limPt (K) (A)$
	limcflf.k	$⊢ K = TopOpen (ℂ_{fld})$
	limcflf.c	$⊢ C = A ∖ \{B\}$
	limcflf.l	$⊢ L = nei (K) (\{B\}) ↾_{𝑡} C$
Assertion	limcflf	$⊢ φ \to F {lim}_{ℂ} B = (K fLimf L) ({F ↾}_{C})$

Proof

Step	Hyp	Ref	Expression
1		limcflf.f	$⊢ φ \to F : A ⟶ ℂ$
2		limcflf.a	$⊢ φ \to A \subseteq ℂ$
3		limcflf.b	$⊢ φ \to B \in limPt (K) (A)$
4		limcflf.k	$⊢ K = TopOpen (ℂ_{fld})$
5		limcflf.c	$⊢ C = A ∖ \{B\}$
6		limcflf.l	$⊢ L = nei (K) (\{B\}) ↾_{𝑡} C$
7		vex	$⊢ t \in V$
8	7	inex1	$⊢ t \cap C \in V$
9	8	rgenw	$⊢ \forall t \in nei (K) (\{B\}) t \cap C \in V$
10		eqid	$⊢ (t \in nei (K) (\{B\}) ⟼ t \cap C) = (t \in nei (K) (\{B\}) ⟼ t \cap C)$
11		imaeq2	$⊢ s = t \cap C \to ({F ↾}_{C}) [s] = ({F ↾}_{C}) [t \cap C]$
12		inss2	$⊢ t \cap C \subseteq C$
13		resima2	$⊢ t \cap C \subseteq C \to ({F ↾}_{C}) [t \cap C] = F [t \cap C]$
14	12 13	ax-mp	$⊢ ({F ↾}_{C}) [t \cap C] = F [t \cap C]$
15	11 14	eqtrdi	$⊢ s = t \cap C \to ({F ↾}_{C}) [s] = F [t \cap C]$
16	15	sseq1d	$⊢ s = t \cap C \to (({F ↾}_{C}) [s] \subseteq u \leftrightarrow F [t \cap C] \subseteq u)$
17	10 16	rexrnmptw	$⊢ \forall t \in nei (K) (\{B\}) t \cap C \in V \to (\exists s \in ran (t \in nei (K) (\{B\}) ⟼ t \cap C) ({F ↾}_{C}) [s] \subseteq u \leftrightarrow \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u)$
18	9 17	mp1i	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to (\exists s \in ran (t \in nei (K) (\{B\}) ⟼ t \cap C) ({F ↾}_{C}) [s] \subseteq u \leftrightarrow \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u)$
19		fvex	$⊢ nei (K) (\{B\}) \in V$
20		difss	$⊢ A ∖ \{B\} \subseteq A$
21	5 20	eqsstri	$⊢ C \subseteq A$
22	21 2	sstrid	$⊢ φ \to C \subseteq ℂ$
23		cnex	$⊢ ℂ \in V$
24	23	ssex	$⊢ C \subseteq ℂ \to C \in V$
25	22 24	syl	$⊢ φ \to C \in V$
26	25	ad2antrr	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to C \in V$
27		restval	$⊢ (nei (K) (\{B\}) \in V \land C \in V) \to nei (K) (\{B\}) ↾_{𝑡} C = ran (t \in nei (K) (\{B\}) ⟼ t \cap C)$
28	19 26 27	sylancr	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to nei (K) (\{B\}) ↾_{𝑡} C = ran (t \in nei (K) (\{B\}) ⟼ t \cap C)$
29	6 28	syl5eq	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to L = ran (t \in nei (K) (\{B\}) ⟼ t \cap C)$
30	29	rexeqdv	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to (\exists s \in L ({F ↾}_{C}) [s] \subseteq u \leftrightarrow \exists s \in ran (t \in nei (K) (\{B\}) ⟼ t \cap C) ({F ↾}_{C}) [s] \subseteq u)$
31	4	cnfldtop	$⊢ K \in Top$
32		opnneip	$⊢ (K \in Top \land w \in K \land B \in w) \to w \in nei (K) (\{B\})$
33	31 32	mp3an1	$⊢ (w \in K \land B \in w) \to w \in nei (K) (\{B\})$
34		id	$⊢ t = w \to t = w$
35	5	a1i	$⊢ t = w \to C = A ∖ \{B\}$
36	34 35	ineq12d	$⊢ t = w \to t \cap C = w \cap (A ∖ \{B\})$
37	36	imaeq2d	$⊢ t = w \to F [t \cap C] = F [w \cap (A ∖ \{B\})]$
38	37	sseq1d	$⊢ t = w \to (F [t \cap C] \subseteq u \leftrightarrow F [w \cap (A ∖ \{B\})] \subseteq u)$
39	38	rspcev	$⊢ (w \in nei (K) (\{B\}) \land F [w \cap (A ∖ \{B\})] \subseteq u) \to \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u$
40	33 39	sylan	$⊢ ((w \in K \land B \in w) \land F [w \cap (A ∖ \{B\})] \subseteq u) \to \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u$
41	40	anasss	$⊢ (w \in K \land (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u)) \to \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u$
42	41	rexlimiva	$⊢ \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u) \to \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u$
43		simprl	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to t \in nei (K) (\{B\})$
44	4	cnfldtopon	$⊢ K \in TopOn (ℂ)$
45	44	toponunii	$⊢ ℂ = ⋃ K$
46	45	neii1	$⊢ (K \in Top \land t \in nei (K) (\{B\})) \to t \subseteq ℂ$
47	31 43 46	sylancr	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to t \subseteq ℂ$
48	45	ntropn	$⊢ (K \in Top \land t \subseteq ℂ) \to int (K) (t) \in K$
49	31 47 48	sylancr	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to int (K) (t) \in K$
50	45	lpss	$⊢ (K \in Top \land A \subseteq ℂ) \to limPt (K) (A) \subseteq ℂ$
51	31 2 50	sylancr	$⊢ φ \to limPt (K) (A) \subseteq ℂ$
52	51 3	sseldd	$⊢ φ \to B \in ℂ$
53	52	snssd	$⊢ φ \to \{B\} \subseteq ℂ$
54	53	ad3antrrr	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to \{B\} \subseteq ℂ$
55	45	neiint	$⊢ (K \in Top \land \{B\} \subseteq ℂ \land t \subseteq ℂ) \to (t \in nei (K) (\{B\}) \leftrightarrow \{B\} \subseteq int (K) (t))$
56	31 54 47 55	mp3an2i	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to (t \in nei (K) (\{B\}) \leftrightarrow \{B\} \subseteq int (K) (t))$
57	43 56	mpbid	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to \{B\} \subseteq int (K) (t)$
58	52	ad3antrrr	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to B \in ℂ$
59		snssg	$⊢ B \in ℂ \to (B \in int (K) (t) \leftrightarrow \{B\} \subseteq int (K) (t))$
60	58 59	syl	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to (B \in int (K) (t) \leftrightarrow \{B\} \subseteq int (K) (t))$
61	57 60	mpbird	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to B \in int (K) (t)$
62	45	ntrss2	$⊢ (K \in Top \land t \subseteq ℂ) \to int (K) (t) \subseteq t$
63	31 47 62	sylancr	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to int (K) (t) \subseteq t$
64		ssrin	$⊢ int (K) (t) \subseteq t \to int (K) (t) \cap C \subseteq t \cap C$
65		imass2	$⊢ int (K) (t) \cap C \subseteq t \cap C \to F [int (K) (t) \cap C] \subseteq F [t \cap C]$
66	63 64 65	3syl	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to F [int (K) (t) \cap C] \subseteq F [t \cap C]$
67		simprr	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to F [t \cap C] \subseteq u$
68	66 67	sstrd	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to F [int (K) (t) \cap C] \subseteq u$
69		eleq2	$⊢ w = int (K) (t) \to (B \in w \leftrightarrow B \in int (K) (t))$
70	5	ineq2i	$⊢ w \cap C = w \cap (A ∖ \{B\})$
71		ineq1	$⊢ w = int (K) (t) \to w \cap C = int (K) (t) \cap C$
72	70 71	eqtr3id	$⊢ w = int (K) (t) \to w \cap (A ∖ \{B\}) = int (K) (t) \cap C$
73	72	imaeq2d	$⊢ w = int (K) (t) \to F [w \cap (A ∖ \{B\})] = F [int (K) (t) \cap C]$
74	73	sseq1d	$⊢ w = int (K) (t) \to (F [w \cap (A ∖ \{B\})] \subseteq u \leftrightarrow F [int (K) (t) \cap C] \subseteq u)$
75	69 74	anbi12d	$⊢ w = int (K) (t) \to ((B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow (B \in int (K) (t) \land F [int (K) (t) \cap C] \subseteq u))$
76	75	rspcev	$⊢ (int (K) (t) \in K \land (B \in int (K) (t) \land F [int (K) (t) \cap C] \subseteq u)) \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u)$
77	49 61 68 76	syl12anc	$⊢ (((φ \land x \in ℂ) \land (u \in K \land x \in u)) \land (t \in nei (K) (\{B\}) \land F [t \cap C] \subseteq u)) \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u)$
78	77	rexlimdvaa	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to (\exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u))$
79	42 78	impbid2	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to (\exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow \exists t \in nei (K) (\{B\}) F [t \cap C] \subseteq u)$
80	18 30 79	3bitr4rd	$⊢ ((φ \land x \in ℂ) \land (u \in K \land x \in u)) \to (\exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow \exists s \in L ({F ↾}_{C}) [s] \subseteq u)$
81	80	anassrs	$⊢ (((φ \land x \in ℂ) \land u \in K) \land x \in u) \to (\exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow \exists s \in L ({F ↾}_{C}) [s] \subseteq u)$
82	81	pm5.74da	$⊢ ((φ \land x \in ℂ) \land u \in K) \to ((x \in u \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u)) \leftrightarrow (x \in u \to \exists s \in L ({F ↾}_{C}) [s] \subseteq u))$
83	82	ralbidva	$⊢ (φ \land x \in ℂ) \to (\forall u \in K (x \in u \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u)) \leftrightarrow \forall u \in K (x \in u \to \exists s \in L ({F ↾}_{C}) [s] \subseteq u))$
84	83	pm5.32da	$⊢ φ \to ((x \in ℂ \land \forall u \in K (x \in u \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u))) \leftrightarrow (x \in ℂ \land \forall u \in K (x \in u \to \exists s \in L ({F ↾}_{C}) [s] \subseteq u)))$
85	1 2 52 4	ellimc2	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow (x \in ℂ \land \forall u \in K (x \in u \to \exists w \in K (B \in w \land F [w \cap (A ∖ \{B\})] \subseteq u))))$
86	1 2 3 4 5 6	limcflflem	$⊢ φ \to L \in Fil (C)$
87		fssres	$⊢ (F : A ⟶ ℂ \land C \subseteq A) \to ({F ↾}_{C}) : C ⟶ ℂ$
88	1 21 87	sylancl	$⊢ φ \to ({F ↾}_{C}) : C ⟶ ℂ$
89		isflf	$⊢ (K \in TopOn (ℂ) \land L \in Fil (C) \land ({F ↾}_{C}) : C ⟶ ℂ) \to (x \in (K fLimf L) ({F ↾}_{C}) \leftrightarrow (x \in ℂ \land \forall u \in K (x \in u \to \exists s \in L ({F ↾}_{C}) [s] \subseteq u)))$
90	44 86 88 89	mp3an2i	$⊢ φ \to (x \in (K fLimf L) ({F ↾}_{C}) \leftrightarrow (x \in ℂ \land \forall u \in K (x \in u \to \exists s \in L ({F ↾}_{C}) [s] \subseteq u)))$
91	84 85 90	3bitr4d	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow x \in (K fLimf L) ({F ↾}_{C}))$
92	91	eqrdv	$⊢ φ \to F {lim}_{ℂ} B = (K fLimf L) ({F ↾}_{C})$

Metamath Proof Explorer

Theorem limcflf

Proof