Definition df-cnext 23119

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 23118	. 2 class CnExt
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 21950	. . 3 class Top
5		vf	. . . 4 setvar 𝑓
6	3	cv 1538	. . . . . 6 class 𝑘
7	6	cuni 4836	. . . . 5 class ∪ 𝑘
8	2	cv 1538	. . . . . 6 class 𝑗
9	8	cuni 4836	. . . . 5 class ∪ 𝑗
10		cpm 8574	. . . . 5 class ↑pm
11	7, 9, 10	co 7255	. . . 4 class (∪ 𝑘 ↑pm ∪ 𝑗)
12		vx	. . . . 5 setvar 𝑥
13	5	cv 1538	. . . . . . 7 class 𝑓
14	13	cdm 5580	. . . . . 6 class dom 𝑓
15		ccl 22077	. . . . . . 7 class cls
16	8, 15	cfv 6418	. . . . . 6 class (cls‘𝑗)
17	14, 16	cfv 6418	. . . . 5 class ((cls‘𝑗)‘dom 𝑓)
18	12	cv 1538	. . . . . . 7 class 𝑥
19	18	csn 4558	. . . . . 6 class {𝑥}
20		cnei 22156	. . . . . . . . . . 11 class nei
21	8, 20	cfv 6418	. . . . . . . . . 10 class (nei‘𝑗)
22	19, 21	cfv 6418	. . . . . . . . 9 class ((nei‘𝑗)‘{𝑥})
23		crest 17048	. . . . . . . . 9 class ↾t
24	22, 14, 23	co 7255	. . . . . . . 8 class (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓)
25		cflf 22994	. . . . . . . 8 class fLimf
26	6, 24, 25	co 7255	. . . . . . 7 class (𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))
27	13, 26	cfv 6418	. . . . . 6 class ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)
28	19, 27	cxp 5578	. . . . 5 class ({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
29	12, 17, 28	ciun 4921	. . . 4 class ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
30	5, 11, 29	cmpt 5153	. . 3 class (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))
31	2, 3, 4, 4, 30	cmpo 7257	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
32	1, 31	wceq 1539	1 wff CnExt = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))

This definition is referenced by:  cnextval  23120