Metamath Proof Explorer


Definition df-fm

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)

Ref Expression
Assertion df-fm
|- FilMap = ( x e. _V , f e. _V |-> ( y e. ( fBas ` dom f ) |-> ( x filGen ran ( t e. y |-> ( f " t ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfm
 |-  FilMap
1 vx
 |-  x
2 cvv
 |-  _V
3 vf
 |-  f
4 vy
 |-  y
5 cfbas
 |-  fBas
6 3 cv
 |-  f
7 6 cdm
 |-  dom f
8 7 5 cfv
 |-  ( fBas ` dom f )
9 1 cv
 |-  x
10 cfg
 |-  filGen
11 vt
 |-  t
12 4 cv
 |-  y
13 11 cv
 |-  t
14 6 13 cima
 |-  ( f " t )
15 11 12 14 cmpt
 |-  ( t e. y |-> ( f " t ) )
16 15 crn
 |-  ran ( t e. y |-> ( f " t ) )
17 9 16 10 co
 |-  ( x filGen ran ( t e. y |-> ( f " t ) ) )
18 4 8 17 cmpt
 |-  ( y e. ( fBas ` dom f ) |-> ( x filGen ran ( t e. y |-> ( f " t ) ) ) )
19 1 3 2 2 18 cmpo
 |-  ( x e. _V , f e. _V |-> ( y e. ( fBas ` dom f ) |-> ( x filGen ran ( t e. y |-> ( f " t ) ) ) ) )
20 0 19 wceq
 |-  FilMap = ( x e. _V , f e. _V |-> ( y e. ( fBas ` dom f ) |-> ( x filGen ran ( t e. y |-> ( f " t ) ) ) ) )