Definition df-fm 22230

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 22225	. 2 class FilMap
2		vx	. . 3 setvar 𝑥
3		vf	. . 3 setvar 𝑓
4		cvv 3437	. . 3 class V
5		vy	. . . 4 setvar 𝑦
6	3	cv 1521	. . . . . 6 class 𝑓
7	6	cdm 5443	. . . . 5 class dom 𝑓
8		cfbas 20215	. . . . 5 class fBas
9	7, 8	cfv 6225	. . . 4 class (fBas‘dom 𝑓)
10	2	cv 1521	. . . . 5 class 𝑥
11		vt	. . . . . . 7 setvar 𝑡
12	5	cv 1521	. . . . . . 7 class 𝑦
13	11	cv 1521	. . . . . . . 8 class 𝑡
14	6, 13	cima 5446	. . . . . . 7 class (𝑓 “ 𝑡)
15	11, 12, 14	cmpt 5041	. . . . . 6 class (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
16	15	crn 5444	. . . . 5 class ran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
17		cfg 20216	. . . . 5 class filGen
18	10, 16, 17	co 7016	. . . 4 class (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))
19	5, 9, 18	cmpt 5041	. . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))))
20	2, 3, 4, 4, 19	cmpo 7018	. 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))
21	1, 20	wceq 1522	1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))

This definition is referenced by:  fmval  22235  fmf  22237