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 23442
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 23437 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3475 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1541 . . . . . 6 class 𝑓
76cdm 5677 . . . . 5 class dom 𝑓
8 cfbas 20932 . . . . 5 class fBas
97, 8cfv 6544 . . . 4 class (fBas‘dom 𝑓)
102cv 1541 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1541 . . . . . . 7 class 𝑦
1311cv 1541 . . . . . . . 8 class 𝑡
146, 13cima 5680 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5232 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5678 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 20933 . . . . 5 class filGen
1810, 16, 17co 7409 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5232 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7411 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1542 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
Colors of variables: wff setvar class
This definition is referenced by:  fmval  23447  fmf  23449
  Copyright terms: Public domain W3C validator