fbflim2

Description: A condition for a filter base B to converge to a point A . Use neighborhoods instead of open neighborhoods. Compare fbflim . (Contributed by FL, 4-Jul-2011) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	fbflim.3	$⊢ F = X filGen B$
	Assertion	fbflim2	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n))$

Proof

Step	Hyp	Ref	Expression
1		fbflim.3	$⊢ F = X filGen B$
2	1	fbflim	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall y \in J (A \in y \to \exists x \in B x \subseteq y)))$
3		topontop	$⊢ J \in TopOn (X) \to J \in Top$
4	3	ad2antrr	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to J \in Top$
5		simpr	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to A \in X$
6		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
7	6	ad2antrr	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to X = ⋃ J$
8	5 7	eleqtrd	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to A \in ⋃ J$
9		eqid	$⊢ ⋃ J = ⋃ J$
10	9	isneip	$⊢ (J \in Top \land A \in ⋃ J) \to (n \in nei (J) (\{A\}) \leftrightarrow (n \subseteq ⋃ J \land \exists y \in J (A \in y \land y \subseteq n)))$
11	4 8 10	syl2anc	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (n \in nei (J) (\{A\}) \leftrightarrow (n \subseteq ⋃ J \land \exists y \in J (A \in y \land y \subseteq n)))$
12		simpr	$⊢ (n \subseteq ⋃ J \land \exists y \in J (A \in y \land y \subseteq n)) \to \exists y \in J (A \in y \land y \subseteq n)$
13	11 12	biimtrdi	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (n \in nei (J) (\{A\}) \to \exists y \in J (A \in y \land y \subseteq n))$
14		r19.29	$⊢ (\forall y \in J (A \in y \to \exists x \in B x \subseteq y) \land \exists y \in J (A \in y \land y \subseteq n)) \to \exists y \in J ((A \in y \to \exists x \in B x \subseteq y) \land (A \in y \land y \subseteq n))$
15		pm3.45	$⊢ (A \in y \to \exists x \in B x \subseteq y) \to ((A \in y \land y \subseteq n) \to (\exists x \in B x \subseteq y \land y \subseteq n))$
16	15	imp	$⊢ ((A \in y \to \exists x \in B x \subseteq y) \land (A \in y \land y \subseteq n)) \to (\exists x \in B x \subseteq y \land y \subseteq n)$
17		sstr2	$⊢ x \subseteq y \to (y \subseteq n \to x \subseteq n)$
18	17	com12	$⊢ y \subseteq n \to (x \subseteq y \to x \subseteq n)$
19	18	reximdv	$⊢ y \subseteq n \to (\exists x \in B x \subseteq y \to \exists x \in B x \subseteq n)$
20	19	impcom	$⊢ (\exists x \in B x \subseteq y \land y \subseteq n) \to \exists x \in B x \subseteq n$
21	16 20	syl	$⊢ ((A \in y \to \exists x \in B x \subseteq y) \land (A \in y \land y \subseteq n)) \to \exists x \in B x \subseteq n$
22	21	rexlimivw	$⊢ \exists y \in J ((A \in y \to \exists x \in B x \subseteq y) \land (A \in y \land y \subseteq n)) \to \exists x \in B x \subseteq n$
23	14 22	syl	$⊢ (\forall y \in J (A \in y \to \exists x \in B x \subseteq y) \land \exists y \in J (A \in y \land y \subseteq n)) \to \exists x \in B x \subseteq n$
24	23	ex	$⊢ \forall y \in J (A \in y \to \exists x \in B x \subseteq y) \to (\exists y \in J (A \in y \land y \subseteq n) \to \exists x \in B x \subseteq n)$
25	13 24	syl9	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (\forall y \in J (A \in y \to \exists x \in B x \subseteq y) \to (n \in nei (J) (\{A\}) \to \exists x \in B x \subseteq n))$
26	25	ralrimdv	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (\forall y \in J (A \in y \to \exists x \in B x \subseteq y) \to \forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n)$
27	4	adantr	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (y \in J \land A \in y)) \to J \in Top$
28		simprl	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (y \in J \land A \in y)) \to y \in J$
29		simprr	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (y \in J \land A \in y)) \to A \in y$
30		opnneip	$⊢ (J \in Top \land y \in J \land A \in y) \to y \in nei (J) (\{A\})$
31	27 28 29 30	syl3anc	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (y \in J \land A \in y)) \to y \in nei (J) (\{A\})$
32		sseq2	$⊢ n = y \to (x \subseteq n \leftrightarrow x \subseteq y)$
33	32	rexbidv	$⊢ n = y \to (\exists x \in B x \subseteq n \leftrightarrow \exists x \in B x \subseteq y)$
34	33	rspcv	$⊢ y \in nei (J) (\{A\}) \to (\forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n \to \exists x \in B x \subseteq y)$
35	31 34	syl	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land (y \in J \land A \in y)) \to (\forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n \to \exists x \in B x \subseteq y)$
36	35	expr	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land y \in J) \to (A \in y \to (\forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n \to \exists x \in B x \subseteq y))$
37	36	com23	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land y \in J) \to (\forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n \to (A \in y \to \exists x \in B x \subseteq y))$
38	37	ralrimdva	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (\forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n \to \forall y \in J (A \in y \to \exists x \in B x \subseteq y))$
39	26 38	impbid	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (\forall y \in J (A \in y \to \exists x \in B x \subseteq y) \leftrightarrow \forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n)$
40	39	pm5.32da	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to ((A \in X \land \forall y \in J (A \in y \to \exists x \in B x \subseteq y)) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n))$
41	2 40	bitrd	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall n \in nei (J) (\{A\}) \exists x \in B x \subseteq n))$

Metamath Proof Explorer

Theorem fbflim2

Proof