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 22835
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 22830 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3408 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1542 . . . . . 6 class 𝑓
76cdm 5551 . . . . 5 class dom 𝑓
8 cfbas 20351 . . . . 5 class fBas
97, 8cfv 6380 . . . 4 class (fBas‘dom 𝑓)
102cv 1542 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1542 . . . . . . 7 class 𝑦
1311cv 1542 . . . . . . . 8 class 𝑡
146, 13cima 5554 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5135 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5552 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 20352 . . . . 5 class filGen
1810, 16, 17co 7213 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5135 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7215 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1543 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  22840  fmf  22842
  Copyright terms: Public domain W3C validator