df-cnext

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

		Ref	Expression
	Assertion	df-cnext	$⊢ CnExt = (j \in Top, k \in Top ⟼ (f \in (⋃ k ↑_{𝑝𝑚} ⋃ j) ⟼ ⋃_{x \in cls (j) (dom f)} (\{x\} \times (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f))))$

Step	Hyp	Ref	Expression
0		ccnext	$class CnExt$
1		vj	$setvar j$
2		ctop	$class Top$
3		vk	$setvar k$
4		vf	$setvar f$
5	3	cv	$setvar k$
6	5	cuni	$class ⋃ k$
7		cpm	$class ↑_{𝑝𝑚}$
8	1	cv	$setvar j$
9	8	cuni	$class ⋃ j$
10	6 9 7	co	$class (⋃ k ↑_{𝑝𝑚} ⋃ j)$
11		vx	$setvar x$
12		ccl	$class cls$
13	8 12	cfv	$class cls (j)$
14	4	cv	$setvar f$
15	14	cdm	$class dom f$
16	15 13	cfv	$class cls (j) (dom f)$
17	11	cv	$setvar x$
18	17	csn	$class \{x\}$
19		cflf	$class fLimf$
20		cnei	$class nei$
21	8 20	cfv	$class nei (j)$
22	18 21	cfv	$class nei (j) (\{x\})$
23		crest	$class ↾_{𝑡}$
24	22 15 23	co	$class (nei (j) (\{x\}) ↾_{𝑡} dom f)$
25	5 24 19	co	$class (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f))$
26	14 25	cfv	$class (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f)$
27	18 26	cxp	$class (\{x\} \times (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f))$
28	11 16 27	ciun	$class ⋃_{x \in cls (j) (dom f)} (\{x\} \times (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f))$
29	4 10 28	cmpt	$class (f \in (⋃ k ↑_{𝑝𝑚} ⋃ j) ⟼ ⋃_{x \in cls (j) (dom f)} (\{x\} \times (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f)))$
30	1 3 2 2 29	cmpo	$class (j \in Top, k \in Top ⟼ (f \in (⋃ k ↑_{𝑝𝑚} ⋃ j) ⟼ ⋃_{x \in cls (j) (dom f)} (\{x\} \times (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f))))$
31	0 30	wceq	$wff CnExt = (j \in Top, k \in Top ⟼ (f \in (⋃ k ↑_{𝑝𝑚} ⋃ j) ⟼ ⋃_{x \in cls (j) (dom f)} (\{x\} \times (k fLimf (nei (j) (\{x\}) ↾_{𝑡} dom f)) (f))))$

Metamath Proof Explorer