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