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 21953
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 21948 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3389 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1636 . . . . . 6 class 𝑓
76cdm 5309 . . . . 5 class dom 𝑓
8 cfbas 19940 . . . . 5 class fBas
97, 8cfv 6099 . . . 4 class (fBas‘dom 𝑓)
102cv 1636 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1636 . . . . . . 7 class 𝑦
1311cv 1636 . . . . . . . 8 class 𝑡
146, 13cima 5312 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 4921 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5310 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 19941 . . . . 5 class filGen
1810, 16, 17co 6872 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 4921 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpt2 6874 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1637 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  21958  fmf  21960
  Copyright terms: Public domain W3C validator