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 21789
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 21784 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3231 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1522 . . . . . 6 class 𝑓
76cdm 5143 . . . . 5 class dom 𝑓
8 cfbas 19782 . . . . 5 class fBas
97, 8cfv 5926 . . . 4 class (fBas‘dom 𝑓)
102cv 1522 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1522 . . . . . . 7 class 𝑦
1311cv 1522 . . . . . . . 8 class 𝑡
146, 13cima 5146 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 4762 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5144 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 19783 . . . . 5 class filGen
1810, 16, 17co 6690 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 4762 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpt2 6692 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1523 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  21794  fmf  21796
  Copyright terms: Public domain W3C validator