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

Definition df-fm 22230
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 = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Distinct variable group:   𝑡,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-fm
StepHypRef Expression
1 cfm 22225 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3437 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1521 . . . . . 6 class 𝑓
76cdm 5443 . . . . 5 class dom 𝑓
8 cfbas 20215 . . . . 5 class fBas
97, 8cfv 6225 . . . 4 class (fBas‘dom 𝑓)
102cv 1521 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1521 . . . . . . 7 class 𝑦
1311cv 1521 . . . . . . . 8 class 𝑡
146, 13cima 5446 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5041 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5444 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 20216 . . . . 5 class filGen
1810, 16, 17co 7016 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5041 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7018 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1522 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  22235  fmf  22237
  Copyright terms: Public domain W3C validator