Definition df-fm 21742

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 21737	. 2 class FilMap
2		vx	. . 3 setvar 𝑥
3		vf	. . 3 setvar 𝑓
4		cvv 3200	. . 3 class V
5		vy	. . . 4 setvar 𝑦
6	3	cv 1482	. . . . . 6 class 𝑓
7	6	cdm 5114	. . . . 5 class dom 𝑓
8		cfbas 19734	. . . . 5 class fBas
9	7, 8	cfv 5888	. . . 4 class (fBas‘dom 𝑓)
10	2	cv 1482	. . . . 5 class 𝑥
11		vt	. . . . . . 7 setvar 𝑡
12	5	cv 1482	. . . . . . 7 class 𝑦
13	11	cv 1482	. . . . . . . 8 class 𝑡
14	6, 13	cima 5117	. . . . . . 7 class (𝑓 “ 𝑡)
15	11, 12, 14	cmpt 4729	. . . . . 6 class (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
16	15	crn 5115	. . . . 5 class ran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))
17		cfg 19735	. . . . 5 class filGen
18	10, 16, 17	co 6650	. . . 4 class (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))
19	5, 9, 18	cmpt 4729	. . 3 class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))))
20	2, 3, 4, 4, 19	cmpt2 6652	. 2 class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))
21	1, 20	wceq 1483	1 wff FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))

This definition is referenced by:  fmval  21747  fmf  21749