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 21552
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 21547 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3173 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1474 . . . . . 6 class 𝑓
76cdm 5038 . . . . 5 class dom 𝑓
8 cfbas 19555 . . . . 5 class fBas
97, 8cfv 5804 . . . 4 class (fBas‘dom 𝑓)
102cv 1474 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1474 . . . . . . 7 class 𝑦
1311cv 1474 . . . . . . . 8 class 𝑡
146, 13cima 5041 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 4643 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5039 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 19556 . . . . 5 class filGen
1810, 16, 17co 6549 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 4643 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpt2 6551 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1475 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  21557  fmf  21559
  Copyright terms: Public domain W3C validator