This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cnext

Description: Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017)

Ref Expression
Assertion df-cnext CnExt = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )

Detailed syntax breakdown

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 𝑓 ) ) ‘ 𝑓 ) ) ) )