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 ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹𝐹 ⊆ 𝒫 𝑋 ) } )