MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnext Structured version   Visualization version   GIF version

Definition df-cnext 21787
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
StepHypRef Expression
1 ccnext 21786 . 2 class CnExt
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 20630 . . 3 class Top
5 vf . . . 4 setvar 𝑓
63cv 1479 . . . . . 6 class 𝑘
76cuni 4407 . . . . 5 class 𝑘
82cv 1479 . . . . . 6 class 𝑗
98cuni 4407 . . . . 5 class 𝑗
10 cpm 7810 . . . . 5 class pm
117, 9, 10co 6610 . . . 4 class ( 𝑘pm 𝑗)
12 vx . . . . 5 setvar 𝑥
135cv 1479 . . . . . . 7 class 𝑓
1413cdm 5079 . . . . . 6 class dom 𝑓
15 ccl 20745 . . . . . . 7 class cls
168, 15cfv 5852 . . . . . 6 class (cls‘𝑗)
1714, 16cfv 5852 . . . . 5 class ((cls‘𝑗)‘dom 𝑓)
1812cv 1479 . . . . . . 7 class 𝑥
1918csn 4153 . . . . . 6 class {𝑥}
20 cnei 20824 . . . . . . . . . . 11 class nei
218, 20cfv 5852 . . . . . . . . . 10 class (nei‘𝑗)
2219, 21cfv 5852 . . . . . . . . 9 class ((nei‘𝑗)‘{𝑥})
23 crest 16013 . . . . . . . . 9 class t
2422, 14, 23co 6610 . . . . . . . 8 class (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓)
25 cflf 21662 . . . . . . . 8 class fLimf
266, 24, 25co 6610 . . . . . . 7 class (𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))
2713, 26cfv 5852 . . . . . 6 class ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)
2819, 27cxp 5077 . . . . 5 class ({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
2912, 17, 28ciun 4490 . . . 4 class 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))
305, 11, 29cmpt 4678 . . 3 class (𝑓 ∈ ( 𝑘pm 𝑗) ↦ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))
312, 3, 4, 4, 30cmpt2 6612 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ ( 𝑘pm 𝑗) ↦ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
321, 31wceq 1480 1 wff CnExt = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ ( 𝑘pm 𝑗) ↦ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  cnextval  21788
  Copyright terms: Public domain W3C validator