This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑋 ) )