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

Metamath Proof Explorer

Theorem cnextfres

Description: F and its extension by continuity agree on the domain of F . (Contributed by Thierry Arnoux, 29-Aug-2020)

Ref Expression
Hypotheses cnextfres.c ⊢ 𝐶 = ∪ 𝐽
cnextfres.b ⊢ 𝐵 = ∪ 𝐾
cnextfres.j ⊢ ( 𝜑 → 𝐽 ∈ Top )
cnextfres.k ⊢ ( 𝜑 → 𝐾 ∈ Haus )
cnextfres.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
cnextfres.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
cnextfres.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion cnextfres ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cnextfres.c ⊢ 𝐶 = ∪ 𝐽
2 cnextfres.b ⊢ 𝐵 = ∪ 𝐾
3 cnextfres.j ⊢ ( 𝜑 → 𝐽 ∈ Top )
4 cnextfres.k ⊢ ( 𝜑 → 𝐾 ∈ Haus )
5 cnextfres.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
6 cnextfres.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
7 cnextfres.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8 eqid ⊢ ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 )
9 8 2 cnf ⊢ ( 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) → 𝐹 : ∪ ( 𝐽 ↾t 𝐴 ) ⟶ 𝐵 )
10 6 9 syl ⊢ ( 𝜑 → 𝐹 : ∪ ( 𝐽 ↾t 𝐴 ) ⟶ 𝐵 )
11 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
12 3 5 11 syl2anc ⊢ ( 𝜑 → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
13 12 feq2d ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : ∪ ( 𝐽 ↾t 𝐴 ) ⟶ 𝐵 ) )
14 10 13 mpbird ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
15 1 2 cnextfun ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
16 3 4 14 5 15 syl22anc ⊢ ( 𝜑 → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
17 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ) → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
18 3 5 17 syl2anc ⊢ ( 𝜑 → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
19 18 7 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
20 1 2 3 5 6 7 flfcntr ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
21 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
22 21 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) )
23 22 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) )
24 23 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) )
25 24 fveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
26 25 opeliunxp2 ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
27 19 20 26 sylanbrc ⊢ ( 𝜑 → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
28 haustop ⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top )
29 4 28 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
30 1 2 cnextfval ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
31 3 29 14 5 30 syl22anc ⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
32 27 31 eleqtrrd ⊢ ( 𝜑 → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
33 df-br ⊢ ( 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ( 𝐹 ‘ 𝑋 ) ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) )
34 32 33 sylibr ⊢ ( 𝜑 → 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ( 𝐹 ‘ 𝑋 ) )
35 funbrfv ⊢ ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) → ( 𝑋 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ( 𝐹 ‘ 𝑋 ) → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) )
36 16 34 35 sylc ⊢ ( 𝜑 → ( ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )