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

Definition df-fm 17628
Description: Define a function that takes a filter to a neighborhood filter of the range. (Since we now allow filter bases to have support smaller than the base set, the function has to come first to ensure that curryings are sets.) (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 20-Jul-2015.)
Assertion
Ref Expression
df-fm  |-  FilMap  =  ( x  e.  _V , 
f  e.  _V  |->  ( y  e.  ( fBas `  dom  f )  |->  ( x filGen ran  (  t  e.  y  |->  ( f
" t ) ) ) ) )
Distinct variable group:    t, f, x, y

Detailed syntax breakdown of Definition df-fm
StepHypRef Expression
1 cfm 17623 . 2  class  FilMap
2 vx . . 3  set  x
3 vf . . 3  set  f
4 cvv 2790 . . 3  class  _V
5 vy . . . 4  set  y
63cv 1623 . . . . . 6  class  f
76cdm 4689 . . . . 5  class  dom  f
8 cfbas 17513 . . . . 5  class  fBas
97, 8cfv 5222 . . . 4  class  ( fBas `  dom  f )
102cv 1623 . . . . 5  class  x
11 vt . . . . . . 7  set  t
125cv 1623 . . . . . . 7  class  y
1311cv 1623 . . . . . . . 8  class  t
146, 13cima 4692 . . . . . . 7  class  ( f
" t )
1511, 12, 14cmpt 4079 . . . . . 6  class  ( t  e.  y  |->  ( f
" t ) )
1615crn 4690 . . . . 5  class  ran  ( 
t  e.  y  |->  ( f " t ) )
17 cfg 17514 . . . . 5  class  filGen
1810, 16, 17co 5820 . . . 4  class  ( x
filGen ran  (  t  e.  y  |->  ( f "
t ) ) )
195, 9, 18cmpt 4079 . . 3  class  ( y  e.  ( fBas `  dom  f )  |->  ( x
filGen ran  (  t  e.  y  |->  ( f "
t ) ) ) )
202, 3, 4, 4, 19cmpt2 5822 . 2  class  ( x  e.  _V ,  f  e.  _V  |->  ( y  e.  ( fBas `  dom  f )  |->  ( x
filGen ran  (  t  e.  y  |->  ( f "
t ) ) ) ) )
211, 20wceq 1624 1  wff  FilMap  =  ( x  e.  _V , 
f  e.  _V  |->  ( y  e.  ( fBas `  dom  f )  |->  ( x filGen ran  (  t  e.  y  |->  ( f
" t ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  fmval  17633  fmf  17635
  Copyright terms: Public domain W3C validator