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