Step |
Hyp |
Ref |
Expression |
0 |
|
ccnext |
⊢ CnExt |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vk |
⊢ 𝑘 |
4 |
|
vf |
⊢ 𝑓 |
5 |
3
|
cv |
⊢ 𝑘 |
6 |
5
|
cuni |
⊢ ∪ 𝑘 |
7 |
|
cpm |
⊢ ↑pm |
8 |
1
|
cv |
⊢ 𝑗 |
9 |
8
|
cuni |
⊢ ∪ 𝑗 |
10 |
6 9 7
|
co |
⊢ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) |
11 |
|
vx |
⊢ 𝑥 |
12 |
|
ccl |
⊢ cls |
13 |
8 12
|
cfv |
⊢ ( cls ‘ 𝑗 ) |
14 |
4
|
cv |
⊢ 𝑓 |
15 |
14
|
cdm |
⊢ dom 𝑓 |
16 |
15 13
|
cfv |
⊢ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) |
17 |
11
|
cv |
⊢ 𝑥 |
18 |
17
|
csn |
⊢ { 𝑥 } |
19 |
|
cflf |
⊢ fLimf |
20 |
|
cnei |
⊢ nei |
21 |
8 20
|
cfv |
⊢ ( nei ‘ 𝑗 ) |
22 |
18 21
|
cfv |
⊢ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) |
23 |
|
crest |
⊢ ↾t |
24 |
22 15 23
|
co |
⊢ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) |
25 |
5 24 19
|
co |
⊢ ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) |
26 |
14 25
|
cfv |
⊢ ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) |
27 |
18 26
|
cxp |
⊢ ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) |
28 |
11 16 27
|
ciun |
⊢ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) |
29 |
4 10 28
|
cmpt |
⊢ ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) |
30 |
1 3 2 2 29
|
cmpo |
⊢ ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) ) |
31 |
0 30
|
wceq |
⊢ CnExt = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) ) |