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 ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )