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 23946
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 23941 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3480 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1539 . . . . . 6 class 𝑓
76cdm 5685 . . . . 5 class dom 𝑓
8 cfbas 21352 . . . . 5 class fBas
97, 8cfv 6561 . . . 4 class (fBas‘dom 𝑓)
102cv 1539 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1539 . . . . . . 7 class 𝑦
1311cv 1539 . . . . . . . 8 class 𝑡
146, 13cima 5688 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5225 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5686 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 21353 . . . . 5 class filGen
1810, 16, 17co 7431 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5225 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7433 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1540 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  23951  fmf  23953
  Copyright terms: Public domain W3C validator