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 ⊢ J ∈ Top ∧ K ∈ Top → J CnExt K = f ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f

Proof

Step Hyp Ref Expression
1 unieq ⊢ j = J → ⋃ j = ⋃ J
2 1 oveq2d ⊢ j = J → ⋃ k ↑ 𝑝𝑚 ⋃ j = ⋃ k ↑ 𝑝𝑚 ⋃ J
3 fveq2 ⊢ j = J → cls ⁡ j = cls ⁡ J
4 3 fveq1d ⊢ j = J → cls ⁡ j ⁡ dom ⁡ f = cls ⁡ J ⁡ dom ⁡ f
5 fveq2 ⊢ j = J → nei ⁡ j = nei ⁡ J
6 5 fveq1d ⊢ j = J → nei ⁡ j ⁡ x = nei ⁡ J ⁡ x
7 6 oveq1d ⊢ j = J → nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f = nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f
8 7 oveq2d ⊢ j = J → k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f = k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f
9 8 fveq1d ⊢ j = J → k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
10 9 xpeq2d ⊢ j = J → x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = x × k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
11 4 10 iuneq12d ⊢ j = J → ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
12 2 11 mpteq12dv ⊢ j = J → f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ j ⟼ ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
13 unieq ⊢ k = K → ⋃ k = ⋃ K
14 13 oveq1d ⊢ k = K → ⋃ k ↑ 𝑝𝑚 ⋃ J = ⋃ K ↑ 𝑝𝑚 ⋃ J
15 oveq1 ⊢ k = K → k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f = K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f
16 15 fveq1d ⊢ k = K → k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
17 16 xpeq2d ⊢ k = K → x × k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
18 17 iuneq2d ⊢ k = K → ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
19 14 18 mpteq12dv ⊢ k = K → f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × k fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = f ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
20 df-cnext ⊢ CnExt = j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ↑ 𝑝𝑚 ⋃ j ⟼ ⋃ x ∈ cls ⁡ j ⁡ dom ⁡ f x × k fLimf nei ⁡ j ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
21 ovex ⊢ ⋃ K ↑ 𝑝𝑚 ⋃ J ∈ V
22 21 mptex ⊢ f ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f ∈ V
23 12 19 20 22 ovmpo ⊢ J ∈ Top ∧ K ∈ Top → J CnExt K = f ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f