Definition df-fm 24074

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 24069	. 2 class FilMap
2		vx	. . 3 setvar 𝑥
3		vf	. . 3 setvar 𝑓
4		cvv 3453	. . 3 class V
5		vy	. . . 4 setvar 𝑦
6	3	cv 1567	. . . . . 6 class 𝑓
7	6	cdm 5661	. . . . 5 class dom 𝑓
8		cfbas 21489	. . . . 5 class fBas
9	7, 8	cfv 6536	. . . 4 class (fBas‘dom 𝑓)
10	2	cv 1567	. . . . 5 class 𝑥
11		vt	. . . . . . 7 setvar 𝑡
12	5	cv 1567	. . . . . . 7 class 𝑦
13	11	cv 1567	. . . . . . . 8 class 𝑡
14	6, 13	cima 5664	. . . . . . 7 class (𝑓 “ 𝑡)
15	11, 12, 14	cmpt 5191	. . . . . 6 class (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
16	15	crn 5662	. . . . 5 class ran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
17		cfg 21490	. . . . 5 class filGen
18	10, 16, 17	co 7410	. . . 4 class (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))
19	5, 9, 18	cmpt 5191	. . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))))
20	2, 3, 4, 4, 19	cmpo 7412	. 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))
21	1, 20	wceq 1568	1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))

This definition is referenced by:  fmval  24079  fmf  24081