Definition df-fm 24284

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

Step	Hyp	Ref	Expression
1		cfm 24279	. 2 class FilMap
2		vx	. . 3 setvar 𝑥
3		vf	. . 3 setvar 𝑓
4		cvv 3454	. . 3 class V
5		vy	. . . 4 setvar 𝑦
6	3	cv 1569	. . . . . 6 class 𝑓
7	6	cdm 5655	. . . . 5 class dom 𝑓
8		cfbas 21693	. . . . 5 class fBas
9	7, 8	cfv 6555	. . . 4 class (fBas‘dom 𝑓)
10	2	cv 1569	. . . . 5 class 𝑥
11		vt	. . . . . . 7 setvar 𝑡
12	5	cv 1569	. . . . . . 7 class 𝑦
13	11	cv 1569	. . . . . . . 8 class 𝑡
14	6, 13	cima 5658	. . . . . . 7 class (𝑓 “ 𝑡)
15	11, 12, 14	cmpt 5189	. . . . . 6 class (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
16	15	crn 5656	. . . . 5 class ran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
17		cfg 21694	. . . . 5 class filGen
18	10, 16, 17	co 7440	. . . 4 class (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))
19	5, 9, 18	cmpt 5189	. . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))))
20	2, 3, 4, 4, 19	cmpo 7442	. 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))
21	1, 20	wceq 1570	1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))

This definition is used by:  fmval  24289  fmf  24291