Definition df-cnext 23563

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

Assertion

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

Distinct variable group:   𝑗,𝑘,𝑓,𝑥

Detailed syntax breakdown of Definition df-cnext

Step	Hyp	Ref	Expression
1		ccnext 23562	. 2 class CnExt
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 22394	. . 3 class Top
5		vf	. . . 4 setvar 𝑓
6	3	cv 1540	. . . . . 6 class 𝑘
7	6	cuni 4908	. . . . 5 class ∪ 𝑘
8	2	cv 1540	. . . . . 6 class 𝑗
9	8	cuni 4908	. . . . 5 class ∪ 𝑗
10		cpm 8820	. . . . 5 class ↑pm
11	7, 9, 10	co 7408	. . . 4 class (∪ 𝑘 ↑pm ∪ 𝑗)
12		vx	. . . . 5 setvar 𝑥
13	5	cv 1540	. . . . . . 7 class 𝑓
14	13	cdm 5676	. . . . . 6 class dom 𝑓
15		ccl 22521	. . . . . . 7 class cls
16	8, 15	cfv 6543	. . . . . 6 class (cls‘𝑗)
17	14, 16	cfv 6543	. . . . 5 class ((cls‘𝑗)‘dom 𝑓)
18	12	cv 1540	. . . . . . 7 class 𝑥
19	18	csn 4628	. . . . . 6 class {𝑥}
20		cnei 22600	. . . . . . . . . . 11 class nei
21	8, 20	cfv 6543	. . . . . . . . . 10 class (nei‘𝑗)
22	19, 21	cfv 6543	. . . . . . . . 9 class ((nei‘𝑗)‘{𝑥})
23		crest 17365	. . . . . . . . 9 class ↾t
24	22, 14, 23	co 7408	. . . . . . . 8 class (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓)
25		cflf 23438	. . . . . . . 8 class fLimf
26	6, 24, 25	co 7408	. . . . . . 7 class (𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))
27	13, 26	cfv 6543	. . . . . 6 class ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)
28	19, 27	cxp 5674	. . . . 5 class ({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
29	12, 17, 28	ciun 4997	. . . 4 class ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
30	5, 11, 29	cmpt 5231	. . 3 class (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))
31	2, 3, 4, 4, 30	cmpo 7410	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
32	1, 31	wceq 1541	1 wff CnExt = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))

This definition is referenced by:  cnextval  23564