Metamath Proof Explorer

Theorem fbflim

Description: A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fbflim.3	$⊢ F = X filGen B$
2		fgcl	$⊢ B \in fBas (X) \to X filGen B \in Fil (X)$
3	1 2	eqeltrid	$⊢ B \in fBas (X) \to F \in Fil (X)$
4		flimopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall x \in J (A \in x \to x \in F)))$
5	3 4	sylan2	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall x \in J (A \in x \to x \in F)))$
6		toponss	$⊢ (J \in TopOn (X) \land x \in J) \to x \subseteq X$
7	6	ad4ant14	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land x \in J) \to x \subseteq X$
8	1	eleq2i	$⊢ x \in F \leftrightarrow x \in (X filGen B)$
9		elfg	$⊢ B \in fBas (X) \to (x \in (X filGen B) \leftrightarrow (x \subseteq X \land \exists y \in B y \subseteq x))$
10	9	ad3antlr	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land x \in J) \to (x \in (X filGen B) \leftrightarrow (x \subseteq X \land \exists y \in B y \subseteq x))$
11	8 10	syl5bb	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land x \in J) \to (x \in F \leftrightarrow (x \subseteq X \land \exists y \in B y \subseteq x))$
12	7 11	mpbirand	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land x \in J) \to (x \in F \leftrightarrow \exists y \in B y \subseteq x)$
13	12	imbi2d	$⊢ (((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \land x \in J) \to ((A \in x \to x \in F) \leftrightarrow (A \in x \to \exists y \in B y \subseteq x))$
14	13	ralbidva	$⊢ ((J \in TopOn (X) \land B \in fBas (X)) \land A \in X) \to (\forall x \in J (A \in x \to x \in F) \leftrightarrow \forall x \in J (A \in x \to \exists y \in B y \subseteq x))$
15	14	pm5.32da	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to ((A \in X \land \forall x \in J (A \in x \to x \in F)) \leftrightarrow (A \in X \land \forall x \in J (A \in x \to \exists y \in B y \subseteq x)))$
16	5 15	bitrd	$⊢ (J \in TopOn (X) \land B \in fBas (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land \forall x \in J (A \in x \to \exists y \in B y \subseteq x)))$