flimopn

Description: The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009) (Proof shortened by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		elflim	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (A \in (J fLim F) \leftrightarrow (A \in X \land nei (J) (\{A\}) \subseteq F))$
2		dfss3	$⊢ nei (J) (\{A\}) \subseteq F \leftrightarrow \forall y \in nei (J) (\{A\}) y \in F$
3		topontop	$⊢ J \in TopOn (X) \to J \in Top$
4	3	ad2antrr	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to J \in Top$
5		opnneip	$⊢ (J \in Top \land x \in J \land A \in x) \to x \in nei (J) (\{A\})$
6	5	3expb	$⊢ (J \in Top \land (x \in J \land A \in x)) \to x \in nei (J) (\{A\})$
7	4 6	sylan	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (x \in J \land A \in x)) \to x \in nei (J) (\{A\})$
8		eleq1	$⊢ y = x \to (y \in F \leftrightarrow x \in F)$
9	8	rspcv	$⊢ x \in nei (J) (\{A\}) \to (\forall y \in nei (J) (\{A\}) y \in F \to x \in F)$
10	7 9	syl	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land (x \in J \land A \in x)) \to (\forall y \in nei (J) (\{A\}) y \in F \to x \in F)$
11	10	expr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land x \in J) \to (A \in x \to (\forall y \in nei (J) (\{A\}) y \in F \to x \in F))$
12	11	com23	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land x \in J) \to (\forall y \in nei (J) (\{A\}) y \in F \to (A \in x \to x \in F))$
13	12	ralrimdva	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (\forall y \in nei (J) (\{A\}) y \in F \to \forall x \in J (A \in x \to x \in F))$
14		simpr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to y \in nei (J) (\{A\})$
15	3	ad3antrrr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to J \in Top$
16		simplr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to A \in X$
17		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
18	17	ad3antrrr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to X = ⋃ J$
19	16 18	eleqtrd	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to A \in ⋃ J$
20	19	snssd	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to \{A\} \subseteq ⋃ J$
21		eqid	$⊢ ⋃ J = ⋃ J$
22	21	neii1	$⊢ (J \in Top \land y \in nei (J) (\{A\})) \to y \subseteq ⋃ J$
23	4 22	sylan	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to y \subseteq ⋃ J$
24	21	neiint	$⊢ (J \in Top \land \{A\} \subseteq ⋃ J \land y \subseteq ⋃ J) \to (y \in nei (J) (\{A\}) \leftrightarrow \{A\} \subseteq int (J) (y))$
25	15 20 23 24	syl3anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to (y \in nei (J) (\{A\}) \leftrightarrow \{A\} \subseteq int (J) (y))$
26	14 25	mpbid	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to \{A\} \subseteq int (J) (y)$
27		snssg	$⊢ A \in X \to (A \in int (J) (y) \leftrightarrow \{A\} \subseteq int (J) (y))$
28	27	ad2antlr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to (A \in int (J) (y) \leftrightarrow \{A\} \subseteq int (J) (y))$
29	26 28	mpbird	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to A \in int (J) (y)$
30	21	ntropn	$⊢ (J \in Top \land y \subseteq ⋃ J) \to int (J) (y) \in J$
31	15 23 30	syl2anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to int (J) (y) \in J$
32		eleq2	$⊢ x = int (J) (y) \to (A \in x \leftrightarrow A \in int (J) (y))$
33		eleq1	$⊢ x = int (J) (y) \to (x \in F \leftrightarrow int (J) (y) \in F)$
34	32 33	imbi12d	$⊢ x = int (J) (y) \to ((A \in x \to x \in F) \leftrightarrow (A \in int (J) (y) \to int (J) (y) \in F))$
35	34	rspcv	$⊢ int (J) (y) \in J \to (\forall x \in J (A \in x \to x \in F) \to (A \in int (J) (y) \to int (J) (y) \in F))$
36	31 35	syl	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to (\forall x \in J (A \in x \to x \in F) \to (A \in int (J) (y) \to int (J) (y) \in F))$
37	29 36	mpid	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to (\forall x \in J (A \in x \to x \in F) \to int (J) (y) \in F)$
38		simpllr	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to F \in Fil (X)$
39	21	ntrss2	$⊢ (J \in Top \land y \subseteq ⋃ J) \to int (J) (y) \subseteq y$
40	15 23 39	syl2anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to int (J) (y) \subseteq y$
41	23 18	sseqtrrd	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to y \subseteq X$
42		filss	$⊢ (F \in Fil (X) \land (int (J) (y) \in F \land y \subseteq X \land int (J) (y) \subseteq y)) \to y \in F$
43	42	3exp2	$⊢ F \in Fil (X) \to (int (J) (y) \in F \to (y \subseteq X \to (int (J) (y) \subseteq y \to y \in F)))$
44	43	com24	$⊢ F \in Fil (X) \to (int (J) (y) \subseteq y \to (y \subseteq X \to (int (J) (y) \in F \to y \in F)))$
45	38 40 41 44	syl3c	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to (int (J) (y) \in F \to y \in F)$
46	37 45	syld	$⊢ (((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \land y \in nei (J) (\{A\})) \to (\forall x \in J (A \in x \to x \in F) \to y \in F)$
47	46	ralrimdva	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (\forall x \in J (A \in x \to x \in F) \to \forall y \in nei (J) (\{A\}) y \in F)$
48	13 47	impbid	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (\forall y \in nei (J) (\{A\}) y \in F \leftrightarrow \forall x \in J (A \in x \to x \in F))$
49	2 48	syl5bb	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land A \in X) \to (nei (J) (\{A\}) \subseteq F \leftrightarrow \forall x \in J (A \in x \to x \in F))$
50	49	pm5.32da	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to ((A \in X \land nei (J) (\{A\}) \subseteq F) \leftrightarrow (A \in X \land \forall x \in J (A \in x \to x \in F)))$
51	1 50	bitrd	$⊢ (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)))$

Metamath Proof Explorer

Theorem flimopn

Proof