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

Metamath Proof Explorer

Theorem flimval

Description: The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion flimval ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐽 fLim 𝐹 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } )

Proof

Step Hyp Ref Expression
1 flimval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
3 2 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → 𝑋 ∈ 𝐽 )
4 rabexg ⊢ ( 𝑋 ∈ 𝐽 → { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ∈ V )
5 3 4 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ∈ V )
6 simpl ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝑗 = 𝐽 )
7 6 unieqd ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∪ 𝑗 = ∪ 𝐽 )
8 7 1 eqtr4di ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∪ 𝑗 = 𝑋 )
9 6 fveq2d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( nei ‘ 𝑗 ) = ( nei ‘ 𝐽 ) )
10 9 fveq1d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
11 simpr ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
12 10 11 sseq12d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ↔ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) )
13 8 pweqd ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝒫 ∪ 𝑗 = 𝒫 𝑋 )
14 11 13 sseq12d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ⊆ 𝒫 ∪ 𝑗 ↔ 𝐹 ⊆ 𝒫 𝑋 ) )
15 12 14 anbi12d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) ) )
16 8 15 rabeqbidv ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } )
17 df-flim ⊢ fLim = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } )
18 16 17 ovmpoga ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ∈ V ) → ( 𝐽 fLim 𝐹 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } )
19 5 18 mpd3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐽 fLim 𝐹 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } )