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 23434
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 23433 . 2 class CnExt
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar π‘˜
4 ctop 22265 . . 3 class Top
5 vf . . . 4 setvar 𝑓
63cv 1541 . . . . . 6 class π‘˜
76cuni 4869 . . . . 5 class βˆͺ π‘˜
82cv 1541 . . . . . 6 class 𝑗
98cuni 4869 . . . . 5 class βˆͺ 𝑗
10 cpm 8772 . . . . 5 class ↑pm
117, 9, 10co 7361 . . . 4 class (βˆͺ π‘˜ ↑pm βˆͺ 𝑗)
12 vx . . . . 5 setvar π‘₯
135cv 1541 . . . . . . 7 class 𝑓
1413cdm 5637 . . . . . 6 class dom 𝑓
15 ccl 22392 . . . . . . 7 class cls
168, 15cfv 6500 . . . . . 6 class (clsβ€˜π‘—)
1714, 16cfv 6500 . . . . 5 class ((clsβ€˜π‘—)β€˜dom 𝑓)
1812cv 1541 . . . . . . 7 class π‘₯
1918csn 4590 . . . . . 6 class {π‘₯}
20 cnei 22471 . . . . . . . . . . 11 class nei
218, 20cfv 6500 . . . . . . . . . 10 class (neiβ€˜π‘—)
2219, 21cfv 6500 . . . . . . . . 9 class ((neiβ€˜π‘—)β€˜{π‘₯})
23 crest 17310 . . . . . . . . 9 class β†Ύt
2422, 14, 23co 7361 . . . . . . . 8 class (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓)
25 cflf 23309 . . . . . . . 8 class fLimf
266, 24, 25co 7361 . . . . . . 7 class (π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))
2713, 26cfv 6500 . . . . . 6 class ((π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))β€˜π‘“)
2819, 27cxp 5635 . . . . 5 class ({π‘₯} Γ— ((π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))β€˜π‘“))
2912, 17, 28ciun 4958 . . . 4 class βˆͺ π‘₯ ∈ ((clsβ€˜π‘—)β€˜dom 𝑓)({π‘₯} Γ— ((π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))β€˜π‘“))
305, 11, 29cmpt 5192 . . 3 class (𝑓 ∈ (βˆͺ π‘˜ ↑pm βˆͺ 𝑗) ↦ βˆͺ π‘₯ ∈ ((clsβ€˜π‘—)β€˜dom 𝑓)({π‘₯} Γ— ((π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))β€˜π‘“)))
312, 3, 4, 4, 30cmpo 7363 . 2 class (𝑗 ∈ Top, π‘˜ ∈ Top ↦ (𝑓 ∈ (βˆͺ π‘˜ ↑pm βˆͺ 𝑗) ↦ βˆͺ π‘₯ ∈ ((clsβ€˜π‘—)β€˜dom 𝑓)({π‘₯} Γ— ((π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))β€˜π‘“))))
321, 31wceq 1542 1 wff CnExt = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ (𝑓 ∈ (βˆͺ π‘˜ ↑pm βˆͺ 𝑗) ↦ βˆͺ π‘₯ ∈ ((clsβ€˜π‘—)β€˜dom 𝑓)({π‘₯} Γ— ((π‘˜ fLimf (((neiβ€˜π‘—)β€˜{π‘₯}) β†Ύt dom 𝑓))β€˜π‘“))))
Colors of variables: wff setvar class
This definition is referenced by:  cnextval  23435
  Copyright terms: Public domain W3C validator