Metamath Proof Explorer


Theorem cnextval

Description: The function applying continuous extension to a given function f . (Contributed by Thierry Arnoux, 1-Dec-2017)

Ref Expression
Assertion cnextval JTopKTopJCnExtK=fK𝑝𝑚JxclsJdomfx×KfLimfneiJx𝑡domff

Proof

Step Hyp Ref Expression
1 unieq j=Jj=J
2 1 oveq2d j=Jk𝑝𝑚j=k𝑝𝑚J
3 fveq2 j=Jclsj=clsJ
4 3 fveq1d j=Jclsjdomf=clsJdomf
5 fveq2 j=Jneij=neiJ
6 5 fveq1d j=Jneijx=neiJx
7 6 oveq1d j=Jneijx𝑡domf=neiJx𝑡domf
8 7 oveq2d j=JkfLimfneijx𝑡domf=kfLimfneiJx𝑡domf
9 8 fveq1d j=JkfLimfneijx𝑡domff=kfLimfneiJx𝑡domff
10 9 xpeq2d j=Jx×kfLimfneijx𝑡domff=x×kfLimfneiJx𝑡domff
11 4 10 iuneq12d j=Jxclsjdomfx×kfLimfneijx𝑡domff=xclsJdomfx×kfLimfneiJx𝑡domff
12 2 11 mpteq12dv j=Jfk𝑝𝑚jxclsjdomfx×kfLimfneijx𝑡domff=fk𝑝𝑚JxclsJdomfx×kfLimfneiJx𝑡domff
13 unieq k=Kk=K
14 13 oveq1d k=Kk𝑝𝑚J=K𝑝𝑚J
15 oveq1 k=KkfLimfneiJx𝑡domf=KfLimfneiJx𝑡domf
16 15 fveq1d k=KkfLimfneiJx𝑡domff=KfLimfneiJx𝑡domff
17 16 xpeq2d k=Kx×kfLimfneiJx𝑡domff=x×KfLimfneiJx𝑡domff
18 17 iuneq2d k=KxclsJdomfx×kfLimfneiJx𝑡domff=xclsJdomfx×KfLimfneiJx𝑡domff
19 14 18 mpteq12dv k=Kfk𝑝𝑚JxclsJdomfx×kfLimfneiJx𝑡domff=fK𝑝𝑚JxclsJdomfx×KfLimfneiJx𝑡domff
20 df-cnext CnExt=jTop,kTopfk𝑝𝑚jxclsjdomfx×kfLimfneijx𝑡domff
21 ovex K𝑝𝑚JV
22 21 mptex fK𝑝𝑚JxclsJdomfx×KfLimfneiJx𝑡domffV
23 12 19 20 22 ovmpo JTopKTopJCnExtK=fK𝑝𝑚JxclsJdomfx×KfLimfneiJx𝑡domff