Metamath Proof Explorer

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 = x ∈ V , f ∈ V ⟼ y ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ t ∈ y ⟼ f t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfm class FilMap
1 vx setvar x
2 cvv class V
3 vf setvar f
4 vy setvar y
5 cfbas class fBas
6 3 cv setvar f
7 6 cdm class dom ⁡ f
8 7 5 cfv class fBas ⁡ dom ⁡ f
9 1 cv setvar x
10 cfg class filGen
11 vt setvar t
12 4 cv setvar y
13 11 cv setvar t
14 6 13 cima class f t
15 11 12 14 cmpt class t ∈ y ⟼ f t
16 15 crn class ran ⁡ t ∈ y ⟼ f t
17 9 16 10 co class x filGen ran ⁡ t ∈ y ⟼ f t
18 4 8 17 cmpt class y ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ t ∈ y ⟼ f t
19 1 3 2 2 18 cmpo class x ∈ V , f ∈ V ⟼ y ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ t ∈ y ⟼ f t
20 0 19 wceq wff FilMap = x ∈ V , f ∈ V ⟼ y ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ t ∈ y ⟼ f t