MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fg Structured version   Visualization version   GIF version

Definition df-fg 19971
Description: Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
Assertion
Ref Expression
df-fg filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
Distinct variable group:   𝑥,𝑦,𝑤

Detailed syntax breakdown of Definition df-fg
StepHypRef Expression
1 cfg 19962 . 2 class filGen
2 vw . . 3 setvar 𝑤
3 vx . . 3 setvar 𝑥
4 cvv 3402 . . 3 class V
52cv 1636 . . . 4 class 𝑤
6 cfbas 19961 . . . 4 class fBas
75, 6cfv 6110 . . 3 class (fBas‘𝑤)
83cv 1636 . . . . . 6 class 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1636 . . . . . . 7 class 𝑦
1110cpw 4362 . . . . . 6 class 𝒫 𝑦
128, 11cin 3779 . . . . 5 class (𝑥 ∩ 𝒫 𝑦)
13 c0 4127 . . . . 5 class
1412, 13wne 2989 . . . 4 wff (𝑥 ∩ 𝒫 𝑦) ≠ ∅
155cpw 4362 . . . 4 class 𝒫 𝑤
1614, 9, 15crab 3111 . . 3 class {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}
172, 3, 4, 7, 16cmpt2 6885 . 2 class (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
181, 17wceq 1637 1 wff filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
Colors of variables: wff setvar class
This definition is referenced by:  fgval  21907  fgabs  21916
  Copyright terms: Public domain W3C validator