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