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 
|- C = U. J
cnextfres.b 
|- B = U. K
cnextfres.j 
|- ( ph -> J e. Top )
cnextfres.k 
|- ( ph -> K e. Haus )
cnextfres.a 
|- ( ph -> A C_ C )
cnextfres.1 
|- ( ph -> F e. ( ( J |`t A ) Cn K ) )
cnextfres.x 
|- ( ph -> X e. A )
Assertion cnextfres 
|- ( ph -> ( ( ( J CnExt K ) ` F ) ` X ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 cnextfres.c 
 |-  C = U. J
2 cnextfres.b 
 |-  B = U. K
3 cnextfres.j 
 |-  ( ph -> J e. Top )
4 cnextfres.k 
 |-  ( ph -> K e. Haus )
5 cnextfres.a 
 |-  ( ph -> A C_ C )
6 cnextfres.1 
 |-  ( ph -> F e. ( ( J |`t A ) Cn K ) )
7 cnextfres.x 
 |-  ( ph -> X e. A )
8 eqid 
 |-  U. ( J |`t A ) = U. ( J |`t A )
9 8 2 cnf 
 |-  ( F e. ( ( J |`t A ) Cn K ) -> F : U. ( J |`t A ) --> B )
10 6 9 syl 
 |-  ( ph -> F : U. ( J |`t A ) --> B )
11 1 restuni 
 |-  ( ( J e. Top /\ A C_ C ) -> A = U. ( J |`t A ) )
12 3 5 11 syl2anc 
 |-  ( ph -> A = U. ( J |`t A ) )
13 12 feq2d 
 |-  ( ph -> ( F : A --> B <-> F : U. ( J |`t A ) --> B ) )
14 10 13 mpbird 
 |-  ( ph -> F : A --> B )
15 1 2 cnextfun 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) )
16 3 4 14 5 15 syl22anc 
 |-  ( ph -> Fun ( ( J CnExt K ) ` F ) )
17 1 sscls 
 |-  ( ( J e. Top /\ A C_ C ) -> A C_ ( ( cls ` J ) ` A ) )
18 3 5 17 syl2anc 
 |-  ( ph -> A C_ ( ( cls ` J ) ` A ) )
19 18 7 sseldd 
 |-  ( ph -> X e. ( ( cls ` J ) ` A ) )
20 1 2 3 5 6 7 flfcntr 
 |-  ( ph -> ( F ` X ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
21 sneq 
 |-  ( x = X -> { x } = { X } )
22 21 fveq2d 
 |-  ( x = X -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { X } ) )
23 22 oveq1d 
 |-  ( x = X -> ( ( ( nei ` J ) ` { x } ) |`t A ) = ( ( ( nei ` J ) ` { X } ) |`t A ) )
24 23 oveq2d 
 |-  ( x = X -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) )
25 24 fveq1d 
 |-  ( x = X -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
26 25 opeliunxp2 
 |-  ( <. X , ( F ` X ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( X e. ( ( cls ` J ) ` A ) /\ ( F ` X ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
27 19 20 26 sylanbrc 
 |-  ( ph -> <. X , ( F ` X ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
28 haustop 
 |-  ( K e. Haus -> K e. Top )
29 4 28 syl 
 |-  ( ph -> K e. Top )
30 1 2 cnextfval 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
31 3 29 14 5 30 syl22anc 
 |-  ( ph -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
32 27 31 eleqtrrd 
 |-  ( ph -> <. X , ( F ` X ) >. e. ( ( J CnExt K ) ` F ) )
33 df-br 
 |-  ( X ( ( J CnExt K ) ` F ) ( F ` X ) <-> <. X , ( F ` X ) >. e. ( ( J CnExt K ) ` F ) )
34 32 33 sylibr 
 |-  ( ph -> X ( ( J CnExt K ) ` F ) ( F ` X ) )
35 funbrfv 
 |-  ( Fun ( ( J CnExt K ) ` F ) -> ( X ( ( J CnExt K ) ` F ) ( F ` X ) -> ( ( ( J CnExt K ) ` F ) ` X ) = ( F ` X ) ) )
36 16 34 35 sylc 
 |-  ( ph -> ( ( ( J CnExt K ) ` F ) ` X ) = ( F ` X ) )