Definition df-cnext 24068

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 24067	. 2 class CnExt
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 22899	. . 3 class Top
5		vf	. . . 4 setvar 𝑓
6	3	cv 1539	. . . . . 6 class 𝑘
7	6	cuni 4907	. . . . 5 class ∪ 𝑘
8	2	cv 1539	. . . . . 6 class 𝑗
9	8	cuni 4907	. . . . 5 class ∪ 𝑗
10		cpm 8867	. . . . 5 class ↑pm
11	7, 9, 10	co 7431	. . . 4 class (∪ 𝑘 ↑pm ∪ 𝑗)
12		vx	. . . . 5 setvar 𝑥
13	5	cv 1539	. . . . . . 7 class 𝑓
14	13	cdm 5685	. . . . . 6 class dom 𝑓
15		ccl 23026	. . . . . . 7 class cls
16	8, 15	cfv 6561	. . . . . 6 class (cls‘𝑗)
17	14, 16	cfv 6561	. . . . 5 class ((cls‘𝑗)‘dom 𝑓)
18	12	cv 1539	. . . . . . 7 class 𝑥
19	18	csn 4626	. . . . . 6 class {𝑥}
20		cnei 23105	. . . . . . . . . . 11 class nei
21	8, 20	cfv 6561	. . . . . . . . . 10 class (nei‘𝑗)
22	19, 21	cfv 6561	. . . . . . . . 9 class ((nei‘𝑗)‘{𝑥})
23		crest 17465	. . . . . . . . 9 class ↾t
24	22, 14, 23	co 7431	. . . . . . . 8 class (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓)
25		cflf 23943	. . . . . . . 8 class fLimf
26	6, 24, 25	co 7431	. . . . . . 7 class (𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))
27	13, 26	cfv 6561	. . . . . 6 class ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)
28	19, 27	cxp 5683	. . . . 5 class ({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
29	12, 17, 28	ciun 4991	. . . 4 class ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
30	5, 11, 29	cmpt 5225	. . 3 class (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))
31	2, 3, 4, 4, 30	cmpo 7433	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
32	1, 31	wceq 1540	1 wff CnExt = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))

This definition is referenced by:  cnextval  24069