Definition df-fm

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)

	Ref	Expression
Assertion	df-fm	⊢ FilMap = ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑦 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfm	⊢ FilMap
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		vy	⊢ 𝑦
5		cfbas	⊢ fBas
6	3	cv	⊢ 𝑓
7	6	cdm	⊢ dom 𝑓
8	7 5	cfv	⊢ ( fBas ‘ dom 𝑓 )
9	1	cv	⊢ 𝑥
10		cfg	⊢ filGen
11		vt	⊢ 𝑡
12	4	cv	⊢ 𝑦
13	11	cv	⊢ 𝑡
14	6 13	cima	⊢ ( 𝑓 “ 𝑡 )
15	11 12 14	cmpt	⊢ ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) )
16	15	crn	⊢ ran ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) )
17	9 16 10	co	⊢ ( 𝑥 filGen ran ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) ) )
18	4 8 17	cmpt	⊢ ( 𝑦 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) ) ) )
19	1 3 2 2 18	cmpo	⊢ ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑦 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) ) ) ) )
20	0 19	wceq	⊢ FilMap = ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑦 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) ) ) ) )