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 22476
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 22471 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3495 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1527 . . . . . 6 class 𝑓
76cdm 5549 . . . . 5 class dom 𝑓
8 cfbas 20463 . . . . 5 class fBas
97, 8cfv 6349 . . . 4 class (fBas‘dom 𝑓)
102cv 1527 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1527 . . . . . . 7 class 𝑦
1311cv 1527 . . . . . . . 8 class 𝑡
146, 13cima 5552 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5138 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5550 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 20464 . . . . 5 class filGen
1810, 16, 17co 7145 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5138 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7147 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1528 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  22481  fmf  22483
  Copyright terms: Public domain W3C validator