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

Definition df-fg 17521
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 17519 . 2  class  filGen
2 vw . . 3  set  w
3 vx . . 3  set  x
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . 4  class  w
6 cfbas 17518 . . . 4  class  fBas
75, 6cfv 5255 . . 3  class  ( fBas `  w )
83cv 1622 . . . . . 6  class  x
9 vy . . . . . . . 8  set  y
109cv 1622 . . . . . . 7  class  y
1110cpw 3625 . . . . . 6  class  ~P y
128, 11cin 3151 . . . . 5  class  ( x  i^i  ~P y )
13 c0 3455 . . . . 5  class  (/)
1412, 13wne 2446 . . . 4  wff  ( x  i^i  ~P y )  =/=  (/)
155cpw 3625 . . . 4  class  ~P w
1614, 9, 15crab 2547 . . 3  class  { y  e.  ~P w  |  ( x  i^i  ~P y )  =/=  (/) }
172, 3, 4, 7, 16cmpt2 5860 . 2  class  ( w  e.  _V ,  x  e.  ( fBas `  w
)  |->  { y  e. 
~P w  |  ( x  i^i  ~P y
)  =/=  (/) } )
181, 17wceq 1623 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  17565  fgabs  17574
  Copyright terms: Public domain W3C validator