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 𝑓 ) ) ‘ 𝑓 ) ) ) )