Definition df-flim

Description: Define a function (indexed by a topology j ) whose value is the limits of a filter f . (Contributed by Jeff Hankins, 4-Sep-2009)

	Ref	Expression
Assertion	df-flim	⊢ fLim = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cflim	⊢ fLim
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vf	⊢ 𝑓
4		cfil	⊢ Fil
5	4	crn	⊢ ran Fil
6	5	cuni	⊢ ∪ ran Fil
7		vx	⊢ 𝑥
8	1	cv	⊢ 𝑗
9	8	cuni	⊢ ∪ 𝑗
10		cnei	⊢ nei
11	8 10	cfv	⊢ ( nei ‘ 𝑗 )
12	7	cv	⊢ 𝑥
13	12	csn	⊢ { 𝑥 }
14	13 11	cfv	⊢ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } )
15	3	cv	⊢ 𝑓
16	14 15	wss	⊢ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓
17	9	cpw	⊢ 𝒫 ∪ 𝑗
18	15 17	wss	⊢ 𝑓 ⊆ 𝒫 ∪ 𝑗
19	16 18	wa	⊢ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 )
20	19 7 9	crab	⊢ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) }
21	1 3 2 6 20	cmpo	⊢ ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } )
22	0 21	wceq	⊢ fLim = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } )