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

Metamath Proof Explorer

Theorem elflim2

Description: The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 flimval.1 ⊢ 𝑋 = ∪ 𝐽
2 anass ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ) )
3 df-3an ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝐹 ⊆ 𝒫 𝑋 ) )
4 3 anbi1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ↔ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
5 df-flim ⊢ fLim = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } )
6 5 elmpocl ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) )
7 1 flimval ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐽 fLim 𝐹 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } )
8 7 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ) )
9 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
10 9 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
11 10 sseq1d ⊢ ( 𝑥 = 𝐴 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ↔ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) )
12 11 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) ) )
13 12 biancomd ⊢ ( 𝑥 = 𝐴 → ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
14 13 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
15 an12 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
16 14 15 bitri ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
17 8 16 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ) )
18 6 17 biadanii ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) ) )
19 2 4 18 3bitr4ri ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )