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 = j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ x ∈ ⋃ j | nei ⁡ j ⁡ x ⊆ f ∧ f ⊆ 𝒫 ⋃ j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cflim class fLim
1 vj setvar j
2 ctop class Top
3 vf setvar f
4 cfil class Fil
5 4 crn class ran ⁡ Fil
6 5 cuni class ⋃ ran ⁡ Fil
7 vx setvar x
8 1 cv setvar j
9 8 cuni class ⋃ j
10 cnei class nei
11 8 10 cfv class nei ⁡ j
12 7 cv setvar x
13 12 csn class x
14 13 11 cfv class nei ⁡ j ⁡ x
15 3 cv setvar f
16 14 15 wss wff nei ⁡ j ⁡ x ⊆ f
17 9 cpw class 𝒫 ⋃ j
18 15 17 wss wff f ⊆ 𝒫 ⋃ j
19 16 18 wa wff nei ⁡ j ⁡ x ⊆ f ∧ f ⊆ 𝒫 ⋃ j
20 19 7 9 crab class x ∈ ⋃ j | nei ⁡ j ⁡ x ⊆ f ∧ f ⊆ 𝒫 ⋃ j
21 1 3 2 6 20 cmpo class j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ x ∈ ⋃ j | nei ⁡ j ⁡ x ⊆ f ∧ f ⊆ 𝒫 ⋃ j
22 0 21 wceq wff fLim = j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ x ∈ ⋃ j | nei ⁡ j ⁡ x ⊆ f ∧ f ⊆ 𝒫 ⋃ j