Metamath Proof Explorer

Theorem cnextfvval

Description: The value of the continuous extension of a given function F at a point X . (Contributed by Thierry Arnoux, 21-Dec-2017)

Ref Expression
Hypotheses cnextf.1 ⊢ C = ⋃ J
cnextf.2 ⊢ B = ⋃ K
cnextf.3 ⊢ φ → J ∈ Top
cnextf.4 ⊢ φ → K ∈ Haus
cnextf.5 ⊢ φ → F : A ⟶ B
cnextf.a ⊢ φ → A ⊆ C
cnextf.6 ⊢ φ → cls ⁡ J ⁡ A = C
cnextf.7 ⊢ φ ∧ x ∈ C → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≠ ∅
Assertion cnextfvval ⊢ φ ∧ X ∈ C → J CnExt K ⁡ F ⁡ X = ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F

Proof

Step Hyp Ref Expression
1 cnextf.1 ⊢ C = ⋃ J
2 cnextf.2 ⊢ B = ⋃ K
3 cnextf.3 ⊢ φ → J ∈ Top
4 cnextf.4 ⊢ φ → K ∈ Haus
5 cnextf.5 ⊢ φ → F : A ⟶ B
6 cnextf.a ⊢ φ → A ⊆ C
7 cnextf.6 ⊢ φ → cls ⁡ J ⁡ A = C
8 cnextf.7 ⊢ φ ∧ x ∈ C → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≠ ∅
9 3 adantr ⊢ φ ∧ X ∈ C → J ∈ Top
10 4 adantr ⊢ φ ∧ X ∈ C → K ∈ Haus
11 5 adantr ⊢ φ ∧ X ∈ C → F : A ⟶ B
12 6 adantr ⊢ φ ∧ X ∈ C → A ⊆ C
13 1 2 cnextfun ⊢ J ∈ Top ∧ K ∈ Haus ∧ F : A ⟶ B ∧ A ⊆ C → Fun ⁡ J CnExt K ⁡ F
14 9 10 11 12 13 syl22anc ⊢ φ ∧ X ∈ C → Fun ⁡ J CnExt K ⁡ F
15 7 eleq2d ⊢ φ → X ∈ cls ⁡ J ⁡ A ↔ X ∈ C
16 15 biimpar ⊢ φ ∧ X ∈ C → X ∈ cls ⁡ J ⁡ A
17 fvex ⊢ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ V
18 17 uniex ⊢ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ V
19 18 snid ⊢ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
20 sneq ⊢ x = X → x = X
21 20 fveq2d ⊢ x = X → nei ⁡ J ⁡ x = nei ⁡ J ⁡ X
22 21 oveq1d ⊢ x = X → nei ⁡ J ⁡ x ↾ 𝑡 A = nei ⁡ J ⁡ X ↾ 𝑡 A
23 22 oveq2d ⊢ x = X → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A = K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A
24 23 fveq1d ⊢ x = X → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F = K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
25 24 breq1d ⊢ x = X → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≈ 1 𝑜 ↔ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ≈ 1 𝑜
26 25 imbi2d ⊢ x = X → φ → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≈ 1 𝑜 ↔ φ → K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ≈ 1 𝑜
27 4 adantr ⊢ φ ∧ x ∈ C → K ∈ Haus
28 3 adantr ⊢ φ ∧ x ∈ C → J ∈ Top
29 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ C
30 28 29 sylib ⊢ φ ∧ x ∈ C → J ∈ TopOn ⁡ C
31 6 adantr ⊢ φ ∧ x ∈ C → A ⊆ C
32 simpr ⊢ φ ∧ x ∈ C → x ∈ C
33 7 eleq2d ⊢ φ → x ∈ cls ⁡ J ⁡ A ↔ x ∈ C
34 33 biimpar ⊢ φ ∧ x ∈ C → x ∈ cls ⁡ J ⁡ A
35 trnei ⊢ J ∈ TopOn ⁡ C ∧ A ⊆ C ∧ x ∈ C → x ∈ cls ⁡ J ⁡ A ↔ nei ⁡ J ⁡ x ↾ 𝑡 A ∈ Fil ⁡ A
36 35 biimpa ⊢ J ∈ TopOn ⁡ C ∧ A ⊆ C ∧ x ∈ C ∧ x ∈ cls ⁡ J ⁡ A → nei ⁡ J ⁡ x ↾ 𝑡 A ∈ Fil ⁡ A
37 30 31 32 34 36 syl31anc ⊢ φ ∧ x ∈ C → nei ⁡ J ⁡ x ↾ 𝑡 A ∈ Fil ⁡ A
38 5 adantr ⊢ φ ∧ x ∈ C → F : A ⟶ B
39 2 hausflf2 ⊢ K ∈ Haus ∧ nei ⁡ J ⁡ x ↾ 𝑡 A ∈ Fil ⁡ A ∧ F : A ⟶ B ∧ K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≠ ∅ → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≈ 1 𝑜
40 27 37 38 8 39 syl31anc ⊢ φ ∧ x ∈ C → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≈ 1 𝑜
41 40 expcom ⊢ x ∈ C → φ → K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ≈ 1 𝑜
42 26 41 vtoclga ⊢ X ∈ C → φ → K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ≈ 1 𝑜
43 42 impcom ⊢ φ ∧ X ∈ C → K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ≈ 1 𝑜
44 en1b ⊢ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ≈ 1 𝑜 ↔ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F = ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
45 43 44 sylib ⊢ φ ∧ X ∈ C → K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F = ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
46 19 45 eleqtrrid ⊢ φ ∧ X ∈ C → ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
47 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
48 47 nfel2 ⊢ Ⅎ x X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
49 nfv ⊢ Ⅎ x X ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
50 48 49 nfbi ⊢ Ⅎ x X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
51 opeq1 ⊢ x = X → x ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F = X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
52 51 eleq1d ⊢ x = X → x ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
53 eleq1 ⊢ x = X → x ∈ cls ⁡ J ⁡ A ↔ X ∈ cls ⁡ J ⁡ A
54 24 eleq2d ⊢ x = X → ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
55 53 54 anbi12d ⊢ x = X → x ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
56 52 55 bibi12d ⊢ x = X → x ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ x ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
57 opeliunxp ⊢ x ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ x ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
58 50 56 57 vtoclg1f ⊢ X ∈ C → X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
59 58 adantl ⊢ φ ∧ X ∈ C → X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F ↔ X ∈ cls ⁡ J ⁡ A ∧ ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
60 16 46 59 mpbir2and ⊢ φ ∧ X ∈ C → X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
61 df-br ⊢ X J CnExt K ⁡ F ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ↔ X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ J CnExt K ⁡ F
62 haustop ⊢ K ∈ Haus → K ∈ Top
63 4 62 syl ⊢ φ → K ∈ Top
64 63 adantr ⊢ φ ∧ X ∈ C → K ∈ Top
65 1 2 cnextfval ⊢ J ∈ Top ∧ K ∈ Top ∧ F : A ⟶ B ∧ A ⊆ C → J CnExt K ⁡ F = ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
66 9 64 11 12 65 syl22anc ⊢ φ ∧ X ∈ C → J CnExt K ⁡ F = ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
67 66 eleq2d ⊢ φ ∧ X ∈ C → X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ J CnExt K ⁡ F ↔ X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
68 61 67 bitrid ⊢ φ ∧ X ∈ C → X J CnExt K ⁡ F ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ↔ X ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ∈ ⋃ x ∈ cls ⁡ J ⁡ A x × K fLimf nei ⁡ J ⁡ x ↾ 𝑡 A ⁡ F
69 60 68 mpbird ⊢ φ ∧ X ∈ C → X J CnExt K ⁡ F ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
70 funbrfv ⊢ Fun ⁡ J CnExt K ⁡ F → X J CnExt K ⁡ F ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F → J CnExt K ⁡ F ⁡ X = ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
71 14 69 70 sylc ⊢ φ ∧ X ∈ C → J CnExt K ⁡ F ⁡ X = ⋃ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F