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	⊢ 𝑋 = ∪ 𝐽
Assertion	flimfil	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		flimuni.1	⊢ 𝑋 = ∪ 𝐽
2	1	elflim2	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
3	2	simplbi	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) )
4	3	simp2d	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ∪ ran Fil )
5		filunirn	⊢ ( 𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
6	4 5	sylib	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
7	3	simp3d	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ⊆ 𝒫 𝑋 )
8		sspwuni	⊢ ( 𝐹 ⊆ 𝒫 𝑋 ↔ ∪ 𝐹 ⊆ 𝑋 )
9	7 8	sylib	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ∪ 𝐹 ⊆ 𝑋 )
10		flimneiss	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 )
11		flimtop	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
12	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
13	11 12	syl	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝑋 ∈ 𝐽 )
14	1	flimelbas	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐴 ∈ 𝑋 )
15		opnneip	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋 ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
16	11 13 14 15	syl3anc	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
17	10 16	sseldd	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝑋 ∈ 𝐹 )
18		elssuni	⊢ ( 𝑋 ∈ 𝐹 → 𝑋 ⊆ ∪ 𝐹 )
19	17 18	syl	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝑋 ⊆ ∪ 𝐹 )
20	9 19	eqssd	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ∪ 𝐹 = 𝑋 )
21	20	fveq2d	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( Fil ‘ ∪ 𝐹 ) = ( Fil ‘ 𝑋 ) )
22	6 21	eleqtrd	⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )