Metamath Proof Explorer

Theorem cnextfval

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

Ref Expression
Hypotheses cnextfval.1 ⊢ X = ⋃ J
cnextfval.2 ⊢ B = ⋃ K
Assertion cnextfval ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → J CnExt K ⁡ F = ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F

Proof

Step Hyp Ref Expression
1 cnextfval.1 ⊢ X = ⋃ J
2 cnextfval.2 ⊢ B = ⋃ K
3 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
4 3 adantr ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → J CnExt K = f ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J ⟼ ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f
5 simpr ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → f = F
6 5 dmeqd ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → dom ⁡ f = dom ⁡ F
7 simplrl ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → F : A ⟶ B
8 7 fdmd ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → dom ⁡ F = A
9 6 8 eqtrd ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → dom ⁡ f = A
10 9 fveq2d ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → cls ⁡ J ⁡ dom ⁡ f = cls ⁡ J ⁡ A
11 9 oveq2d ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f = nei ⁡ J ⁡ x ↾ 𝑡 A
12 11 oveq2d ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f = K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A
13 12 5 fveq12d ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
14 13 xpeq2d ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
15 10 14 iuneq12d ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X ∧ f = F → ⋃ x ∈ cls ⁡ J ⁡ dom ⁡ f x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 dom ⁡ f ⁡ f = ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
16 uniexg ⊢ K ∈ Top → ⋃ K ∈ V
17 16 ad2antlr ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → ⋃ K ∈ V
18 uniexg ⊢ J ∈ Top → ⋃ J ∈ V
19 18 ad2antrr ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → ⋃ J ∈ V
20 eqid ⊢ A = A
21 20 2 feq23i ⊢ F : A ⟶ B ↔ F : A ⟶ ⋃ K
22 21 biimpi ⊢ F : A ⟶ B → F : A ⟶ ⋃ K
23 22 ad2antrl ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → F : A ⟶ ⋃ K
24 1 sseq2i ⊢ A ⊆ X ↔ A ⊆ ⋃ J
25 24 biimpi ⊢ A ⊆ X → A ⊆ ⋃ J
26 25 ad2antll ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → A ⊆ ⋃ J
27 elpm2r ⊢ ⋃ K ∈ V ∧ ⋃ J ∈ V ∧ F : A ⟶ ⋃ K ∧ A ⊆ ⋃ J → F ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J
28 17 19 23 26 27 syl22anc ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → F ∈ ⋃ K ↑ 𝑝𝑚 ⋃ J
29 fvex ⊢ cls ⁡ J ⁡ A ∈ V
30 snex ⊢ x ∈ V
31 fvex ⊢ K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ∈ V
32 30 31 xpex ⊢ x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ∈ V
33 29 32 iunex ⊢ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ∈ V
34 33 a1i ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ∈ V
35 4 15 28 34 fvmptd ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ X → J CnExt K ⁡ F = ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F