Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fm Structured version   Visualization version   GIF version

Definition df-fm 22553
 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 22548 . 2 class FilMap
2 vx . . 3 setvar 𝑥
3 vf . . 3 setvar 𝑓
4 cvv 3441 . . 3 class V
5 vy . . . 4 setvar 𝑦
63cv 1537 . . . . . 6 class 𝑓
76cdm 5520 . . . . 5 class dom 𝑓
8 cfbas 20083 . . . . 5 class fBas
97, 8cfv 6325 . . . 4 class (fBas‘dom 𝑓)
102cv 1537 . . . . 5 class 𝑥
11 vt . . . . . . 7 setvar 𝑡
125cv 1537 . . . . . . 7 class 𝑦
1311cv 1537 . . . . . . . 8 class 𝑡
146, 13cima 5523 . . . . . . 7 class (𝑓𝑡)
1511, 12, 14cmpt 5111 . . . . . 6 class (𝑡𝑦 ↦ (𝑓𝑡))
1615crn 5521 . . . . 5 class ran (𝑡𝑦 ↦ (𝑓𝑡))
17 cfg 20084 . . . . 5 class filGen
1810, 16, 17co 7136 . . . 4 class (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))
195, 9, 18cmpt 5111 . . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡))))
202, 3, 4, 4, 19cmpo 7138 . 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
211, 20wceq 1538 1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡𝑦 ↦ (𝑓𝑡)))))
 Colors of variables: wff setvar class This definition is referenced by:  fmval  22558  fmf  22560
 Copyright terms: Public domain W3C validator