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

Definition df-fg 17515
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  =  ( w  e.  _V ,  x  e.  ( fBas `  w )  |->  { y  e.  ~P w  |  ( x  i^i  ~P y )  =/=  (/) } )
Distinct variable group:    x, w, y

Detailed syntax breakdown of Definition df-fg
StepHypRef Expression
1 cfg 17513 . 2  class  filGen
2 vw . . 3  set  w
3 vx . . 3  set  x
4 cvv 2789 . . 3  class  _V
52cv 1623 . . . 4  class  w
6 cfbas 17512 . . . 4  class  fBas
75, 6cfv 5221 . . 3  class  ( fBas `  w )
83cv 1623 . . . . . 6  class  x
9 vy . . . . . . . 8  set  y
109cv 1623 . . . . . . 7  class  y
1110cpw 3626 . . . . . 6  class  ~P y
128, 11cin 3152 . . . . 5  class  ( x  i^i  ~P y )
13 c0 3456 . . . . 5  class  (/)
1412, 13wne 2447 . . . 4  wff  ( x  i^i  ~P y )  =/=  (/)
155cpw 3626 . . . 4  class  ~P w
1614, 9, 15crab 2548 . . 3  class  { y  e.  ~P w  |  ( x  i^i  ~P y )  =/=  (/) }
172, 3, 4, 7, 16cmpt2 5821 . 2  class  ( w  e.  _V ,  x  e.  ( fBas `  w
)  |->  { y  e. 
~P w  |  ( x  i^i  ~P y
)  =/=  (/) } )
181, 17wceq 1624 1  wff  filGen  =  ( w  e.  _V ,  x  e.  ( fBas `  w )  |->  { y  e.  ~P w  |  ( x  i^i  ~P y )  =/=  (/) } )
Colors of variables: wff set class
This definition is referenced by:  fgval  17559  fgabs  17568
  Copyright terms: Public domain W3C validator