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 23961
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 23956 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3477 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1535 . . . . . 6 class 𝑓
76cdm 5688 . . . . 5 class dom 𝑓
8 cfbas 21369 . . . . 5 class fBas
97, 8cfv 6562 . . . 4 class (fBas‘dom 𝑓)
102cv 1535 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1535 . . . . . . 7 class 𝑦
1311cv 1535 . . . . . . . 8 class 𝑡
146, 13cima 5691 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5230 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5689 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 21370 . . . . 5 class filGen
1810, 16, 17co 7430 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5230 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7432 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1536 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  23966  fmf  23968
  Copyright terms: Public domain W3C validator