This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnExt 𝐾 ) = ( 𝑓 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )

Proof

Step Hyp Ref Expression
1 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
2 1 oveq2d ⊢ ( 𝑗 = 𝐽 → ( ∪ 𝑘 ↑pm ∪ 𝑗 ) = ( ∪ 𝑘 ↑pm ∪ 𝐽 ) )
3 fveq2 ⊢ ( 𝑗 = 𝐽 → ( cls ‘ 𝑗 ) = ( cls ‘ 𝐽 ) )
4 3 fveq1d ⊢ ( 𝑗 = 𝐽 → ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) = ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) )
5 fveq2 ⊢ ( 𝑗 = 𝐽 → ( nei ‘ 𝑗 ) = ( nei ‘ 𝐽 ) )
6 5 fveq1d ⊢ ( 𝑗 = 𝐽 → ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
7 6 oveq1d ⊢ ( 𝑗 = 𝐽 → ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) )
8 7 oveq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) = ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) )
9 8 fveq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) = ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) )
10 9 xpeq2d ⊢ ( 𝑗 = 𝐽 → ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) )
11 4 10 iuneq12d ⊢ ( 𝑗 = 𝐽 → ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) )
12 2 11 mpteq12dv ⊢ ( 𝑗 = 𝐽 → ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) = ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )
13 unieq ⊢ ( 𝑘 = 𝐾 → ∪ 𝑘 = ∪ 𝐾 )
14 13 oveq1d ⊢ ( 𝑘 = 𝐾 → ( ∪ 𝑘 ↑pm ∪ 𝐽 ) = ( ∪ 𝐾 ↑pm ∪ 𝐽 ) )
15 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) )
16 15 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) )
17 16 xpeq2d ⊢ ( 𝑘 = 𝐾 → ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) )
18 17 iuneq2d ⊢ ( 𝑘 = 𝐾 → ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) )
19 14 18 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) = ( 𝑓 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )
20 df-cnext ⊢ CnExt = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑓 ∈ ( ∪ 𝑘 ↑pm ∪ 𝑗 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝑗 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑘 fLimf ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )
21 ovex ⊢ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ∈ V
22 21 mptex ⊢ ( 𝑓 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) ∈ V
23 12 19 20 22 ovmpo ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnExt 𝐾 ) = ( 𝑓 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) )