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

Metamath Proof Explorer

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 ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } )