Step |
Hyp |
Ref |
Expression |
0 |
|
cflf |
⊢ fLimf |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
ctop |
⊢ Top |
3 |
|
vy |
⊢ 𝑦 |
4 |
|
cfil |
⊢ Fil |
5 |
4
|
crn |
⊢ ran Fil |
6 |
5
|
cuni |
⊢ ∪ ran Fil |
7 |
|
vf |
⊢ 𝑓 |
8 |
1
|
cv |
⊢ 𝑥 |
9 |
8
|
cuni |
⊢ ∪ 𝑥 |
10 |
|
cmap |
⊢ ↑m |
11 |
3
|
cv |
⊢ 𝑦 |
12 |
11
|
cuni |
⊢ ∪ 𝑦 |
13 |
9 12 10
|
co |
⊢ ( ∪ 𝑥 ↑m ∪ 𝑦 ) |
14 |
|
cflim |
⊢ fLim |
15 |
|
cfm |
⊢ FilMap |
16 |
7
|
cv |
⊢ 𝑓 |
17 |
9 16 15
|
co |
⊢ ( ∪ 𝑥 FilMap 𝑓 ) |
18 |
11 17
|
cfv |
⊢ ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) |
19 |
8 18 14
|
co |
⊢ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) |
20 |
7 13 19
|
cmpt |
⊢ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) |
21 |
1 3 2 6 20
|
cmpo |
⊢ ( 𝑥 ∈ Top , 𝑦 ∈ ∪ ran Fil ↦ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) ) |
22 |
0 21
|
wceq |
⊢ fLimf = ( 𝑥 ∈ Top , 𝑦 ∈ ∪ ran Fil ↦ ( 𝑓 ∈ ( ∪ 𝑥 ↑m ∪ 𝑦 ) ↦ ( 𝑥 fLim ( ( ∪ 𝑥 FilMap 𝑓 ) ‘ 𝑦 ) ) ) ) |