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

Definition df-fm 17970
 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
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-fm
StepHypRef Expression
1 cfm 17965 . 2
2 vx . . 3
3 vf . . 3
4 cvv 2956 . . 3
5 vy . . . 4
63cv 1651 . . . . . 6
76cdm 4878 . . . . 5
8 cfbas 16689 . . . . 5
97, 8cfv 5454 . . . 4
102cv 1651 . . . . 5
11 vt . . . . . . 7
125cv 1651 . . . . . . 7
1311cv 1651 . . . . . . . 8
146, 13cima 4881 . . . . . . 7
1511, 12, 14cmpt 4266 . . . . . 6
1615crn 4879 . . . . 5
17 cfg 16690 . . . . 5
1810, 16, 17co 6081 . . . 4
195, 9, 18cmpt 4266 . . 3
202, 3, 4, 4, 19cmpt2 6083 . 2
211, 20wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  fmval  17975  fmf  17977
 Copyright terms: Public domain W3C validator