Theorem 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 = U. J
Assertion	flimfil	|- ( A e. ( J fLim F ) -> F e. ( Fil ` X ) )

Proof

Step	Hyp	Ref	Expression
1		flimuni.1	|- X = U. J
2	1	elflim2	|- ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
3	2	simplbi	|- ( A e. ( J fLim F ) -> ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) )
4	3	simp2d	|- ( A e. ( J fLim F ) -> F e. U. ran Fil )
5		filunirn	|- ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )
6	4 5	sylib	|- ( A e. ( J fLim F ) -> F e. ( Fil ` U. F ) )
7	3	simp3d	|- ( A e. ( J fLim F ) -> F C_ ~P X )
8		sspwuni	|- ( F C_ ~P X <-> U. F C_ X )
9	7 8	sylib	|- ( A e. ( J fLim F ) -> U. F C_ X )
10		flimneiss	|- ( A e. ( J fLim F ) -> ( ( nei ` J ) ` { A } ) C_ F )
11		flimtop	|- ( A e. ( J fLim F ) -> J e. Top )
12	1	topopn	|- ( J e. Top -> X e. J )
13	11 12	syl	|- ( A e. ( J fLim F ) -> X e. J )
14	1	flimelbas	|- ( A e. ( J fLim F ) -> A e. X )
15		opnneip	|- ( ( J e. Top /\ X e. J /\ A e. X ) -> X e. ( ( nei ` J ) ` { A } ) )
16	11 13 14 15	syl3anc	|- ( A e. ( J fLim F ) -> X e. ( ( nei ` J ) ` { A } ) )
17	10 16	sseldd	|- ( A e. ( J fLim F ) -> X e. F )
18		elssuni	|- ( X e. F -> X C_ U. F )
19	17 18	syl	|- ( A e. ( J fLim F ) -> X C_ U. F )
20	9 19	eqssd	|- ( A e. ( J fLim F ) -> U. F = X )
21	20	fveq2d	|- ( A e. ( J fLim F ) -> ( Fil ` U. F ) = ( Fil ` X ) )
22	6 21	eleqtrd	|- ( A e. ( J fLim F ) -> F e. ( Fil ` X ) )