Metamath Proof Explorer

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 = j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ j ⟼ ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f

Detailed syntax breakdown

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 × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
28 11 16 27 ciun class ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
29 4 10 28 cmpt class f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ j ⟼ ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
30 1 3 2 2 29 cmpo class j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ j ⟼ ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
31 0 30 wceq wff CnExt = j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ j ⟼ ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f