flimfil

Description: Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	flimuni.1	$⊢ X = ⋃ J$
	Assertion	flimfil	$⊢ A \in (J fLim F) \to F \in Fil (X)$

Step	Hyp	Ref	Expression
1		flimuni.1	$⊢ X = ⋃ J$
2	1	elflim2	$⊢ A \in (J fLim F) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 X) \land (A \in X \land nei (J) (\{A\}) \subseteq F))$
3	2	simplbi	$⊢ A \in (J fLim F) \to (J \in Top \land F \in ⋃ ran Fil \land F \subseteq 𝒫 X)$
4	3	simp2d	$⊢ A \in (J fLim F) \to F \in ⋃ ran Fil$
5		filunirn	$⊢ F \in ⋃ ran Fil \leftrightarrow F \in Fil (⋃ F)$
6	4 5	sylib	$⊢ A \in (J fLim F) \to F \in Fil (⋃ F)$
7	3	simp3d	$⊢ A \in (J fLim F) \to F \subseteq 𝒫 X$
8		sspwuni	$⊢ F \subseteq 𝒫 X \leftrightarrow ⋃ F \subseteq X$
9	7 8	sylib	$⊢ A \in (J fLim F) \to ⋃ F \subseteq X$
10		flimneiss	$⊢ A \in (J fLim F) \to nei (J) (\{A\}) \subseteq F$
11		flimtop	$⊢ A \in (J fLim F) \to J \in Top$
12	1	topopn	$⊢ J \in Top \to X \in J$
13	11 12	syl	$⊢ A \in (J fLim F) \to X \in J$
14	1	flimelbas	$⊢ A \in (J fLim F) \to A \in X$
15		opnneip	$⊢ (J \in Top \land X \in J \land A \in X) \to X \in nei (J) (\{A\})$
16	11 13 14 15	syl3anc	$⊢ A \in (J fLim F) \to X \in nei (J) (\{A\})$
17	10 16	sseldd	$⊢ A \in (J fLim F) \to X \in F$
18		elssuni	$⊢ X \in F \to X \subseteq ⋃ F$
19	17 18	syl	$⊢ A \in (J fLim F) \to X \subseteq ⋃ F$
20	9 19	eqssd	$⊢ A \in (J fLim F) \to ⋃ F = X$
21	20	fveq2d	$⊢ A \in (J fLim F) \to Fil (⋃ F) = Fil (X)$
22	6 21	eleqtrd	$⊢ A \in (J fLim F) \to F \in Fil (X)$

Metamath Proof Explorer