This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Filters and filter bases Filter limits df-fm
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 ( 𝑡 ∈ 𝑦 ↦ ( 𝑓 “ 𝑡 ) ) ) ) )