Step |
Hyp |
Ref |
Expression |
0 |
|
ctsu |
⊢ tsums |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
vf |
⊢ 𝑓 |
4 |
3
|
cv |
⊢ 𝑓 |
5 |
4
|
cdm |
⊢ dom 𝑓 |
6 |
5
|
cpw |
⊢ 𝒫 dom 𝑓 |
7 |
|
cfn |
⊢ Fin |
8 |
6 7
|
cin |
⊢ ( 𝒫 dom 𝑓 ∩ Fin ) |
9 |
|
vs |
⊢ 𝑠 |
10 |
|
ctopn |
⊢ TopOpen |
11 |
1
|
cv |
⊢ 𝑤 |
12 |
11 10
|
cfv |
⊢ ( TopOpen ‘ 𝑤 ) |
13 |
|
cflf |
⊢ fLimf |
14 |
9
|
cv |
⊢ 𝑠 |
15 |
|
cfg |
⊢ filGen |
16 |
|
vz |
⊢ 𝑧 |
17 |
|
vy |
⊢ 𝑦 |
18 |
16
|
cv |
⊢ 𝑧 |
19 |
17
|
cv |
⊢ 𝑦 |
20 |
18 19
|
wss |
⊢ 𝑧 ⊆ 𝑦 |
21 |
20 17 14
|
crab |
⊢ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } |
22 |
16 14 21
|
cmpt |
⊢ ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) |
23 |
22
|
crn |
⊢ ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) |
24 |
14 23 15
|
co |
⊢ ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) |
25 |
12 24 13
|
co |
⊢ ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) |
26 |
|
cgsu |
⊢ Σg |
27 |
4 19
|
cres |
⊢ ( 𝑓 ↾ 𝑦 ) |
28 |
11 27 26
|
co |
⊢ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) |
29 |
17 14 28
|
cmpt |
⊢ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) |
30 |
29 25
|
cfv |
⊢ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) |
31 |
9 8 30
|
csb |
⊢ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) |
32 |
1 3 2 2 31
|
cmpo |
⊢ ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) ) |
33 |
0 32
|
wceq |
⊢ tsums = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) ) |