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 23762
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 23757 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3473 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1539 . . . . . 6 class 𝑓
76cdm 5676 . . . . 5 class dom 𝑓
8 cfbas 21221 . . . . 5 class fBas
97, 8cfv 6543 . . . 4 class (fBas‘dom 𝑓)
102cv 1539 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1539 . . . . . . 7 class 𝑦
1311cv 1539 . . . . . . . 8 class 𝑡
146, 13cima 5679 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5231 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5677 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 21222 . . . . 5 class filGen
1810, 16, 17co 7412 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5231 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7414 . 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  23767  fmf  23769
  Copyright terms: Public domain W3C validator