Metamath Proof Explorer

Theorem cnextfres1

Description: F and its extension by continuity agree on the domain of F . (Contributed by Thierry Arnoux, 17-Jan-2018)

Ref Expression
Hypotheses cnextf.1 
|- C = U. J
cnextf.2 
|- B = U. K
cnextf.3 
|- ( ph -> J e. Top )
cnextf.4 
|- ( ph -> K e. Haus )
cnextf.5 
|- ( ph -> F : A --> B )
cnextf.a 
|- ( ph -> A C_ C )
cnextf.6 
|- ( ph -> ( ( cls ` J ) ` A ) = C )
cnextf.7 
|- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) )
cnextcn.8 
|- ( ph -> K e. Reg )
cnextfres1.1 
|- ( ph -> F e. ( ( J |`t A ) Cn K ) )
Assertion cnextfres1 
|- ( ph -> ( ( ( J CnExt K ) ` F ) |` A ) = F )

Proof

Step Hyp Ref Expression
1 cnextf.1 
 |-  C = U. J
2 cnextf.2 
 |-  B = U. K
3 cnextf.3 
 |-  ( ph -> J e. Top )
4 cnextf.4 
 |-  ( ph -> K e. Haus )
5 cnextf.5 
 |-  ( ph -> F : A --> B )
6 cnextf.a 
 |-  ( ph -> A C_ C )
7 cnextf.6 
 |-  ( ph -> ( ( cls ` J ) ` A ) = C )
8 cnextf.7 
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) )
9 cnextcn.8 
 |-  ( ph -> K e. Reg )
10 cnextfres1.1 
 |-  ( ph -> F e. ( ( J |`t A ) Cn K ) )
11 1 2 3 4 5 6 7 8 cnextf 
 |-  ( ph -> ( ( J CnExt K ) ` F ) : C --> B )
12 11 ffnd 
 |-  ( ph -> ( ( J CnExt K ) ` F ) Fn C )
13 fnssres 
 |-  ( ( ( ( J CnExt K ) ` F ) Fn C /\ A C_ C ) -> ( ( ( J CnExt K ) ` F ) |` A ) Fn A )
14 12 6 13 syl2anc 
 |-  ( ph -> ( ( ( J CnExt K ) ` F ) |` A ) Fn A )
15 5 ffnd 
 |-  ( ph -> F Fn A )
16 fvres 
 |-  ( y e. A -> ( ( ( ( J CnExt K ) ` F ) |` A ) ` y ) = ( ( ( J CnExt K ) ` F ) ` y ) )
17 16 adantl 
 |-  ( ( ph /\ y e. A ) -> ( ( ( ( J CnExt K ) ` F ) |` A ) ` y ) = ( ( ( J CnExt K ) ` F ) ` y ) )
18 6 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. C )
19 1 2 3 4 5 6 7 8 cnextfvval 
 |-  ( ( ph /\ y e. C ) -> ( ( ( J CnExt K ) ` F ) ` y ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) )
20 18 19 syldan 
 |-  ( ( ph /\ y e. A ) -> ( ( ( J CnExt K ) ` F ) ` y ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) )
21 5 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. B )
22 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
23 1 restuni 
 |-  ( ( J e. Top /\ A C_ C ) -> A = U. ( J |`t A ) )
24 3 6 23 syl2anc 
 |-  ( ph -> A = U. ( J |`t A ) )
25 24 adantr 
 |-  ( ( ph /\ y e. A ) -> A = U. ( J |`t A ) )
26 22 25 eleqtrd 
 |-  ( ( ph /\ y e. A ) -> y e. U. ( J |`t A ) )
27 fvex 
 |-  ( ( cls ` J ) ` A ) e. _V
28 7 27 eqeltrrdi 
 |-  ( ph -> C e. _V )
29 28 6 ssexd 
 |-  ( ph -> A e. _V )
30 resttop 
 |-  ( ( J e. Top /\ A e. _V ) -> ( J |`t A ) e. Top )
31 3 29 30 syl2anc 
 |-  ( ph -> ( J |`t A ) e. Top )
32 haustop 
 |-  ( K e. Haus -> K e. Top )
33 4 32 syl 
 |-  ( ph -> K e. Top )
34 24 feq2d 
 |-  ( ph -> ( F : A --> B <-> F : U. ( J |`t A ) --> B ) )
35 5 34 mpbid 
 |-  ( ph -> F : U. ( J |`t A ) --> B )
36 eqid 
 |-  U. ( J |`t A ) = U. ( J |`t A )
37 36 2 cnnei 
 |-  ( ( ( J |`t A ) e. Top /\ K e. Top /\ F : U. ( J |`t A ) --> B ) -> ( F e. ( ( J |`t A ) Cn K ) <-> A. y e. U. ( J |`t A ) A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w ) )
38 31 33 35 37 syl3anc 
 |-  ( ph -> ( F e. ( ( J |`t A ) Cn K ) <-> A. y e. U. ( J |`t A ) A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w ) )
39 10 38 mpbid 
 |-  ( ph -> A. y e. U. ( J |`t A ) A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w )
40 39 r19.21bi 
 |-  ( ( ph /\ y e. U. ( J |`t A ) ) -> A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w )
41 26 40 syldan 
 |-  ( ( ph /\ y e. A ) -> A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w )
42 41 r19.21bi 
 |-  ( ( ( ph /\ y e. A ) /\ w e. ( ( nei ` K ) ` { ( F ` y ) } ) ) -> E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w )
43 snssi 
 |-  ( y e. A -> { y } C_ A )
44 1 neitr 
 |-  ( ( J e. Top /\ A C_ C /\ { y } C_ A ) -> ( ( nei ` ( J |`t A ) ) ` { y } ) = ( ( ( nei ` J ) ` { y } ) |`t A ) )
45 3 6 43 44 syl2an3an 
 |-  ( ( ph /\ y e. A ) -> ( ( nei ` ( J |`t A ) ) ` { y } ) = ( ( ( nei ` J ) ` { y } ) |`t A ) )
46 45 rexeqdv 
 |-  ( ( ph /\ y e. A ) -> ( E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w <-> E. v e. ( ( ( nei ` J ) ` { y } ) |`t A ) ( F " v ) C_ w ) )
47 46 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ w e. ( ( nei ` K ) ` { ( F ` y ) } ) ) -> ( E. v e. ( ( nei ` ( J |`t A ) ) ` { y } ) ( F " v ) C_ w <-> E. v e. ( ( ( nei ` J ) ` { y } ) |`t A ) ( F " v ) C_ w ) )
48 42 47 mpbid 
 |-  ( ( ( ph /\ y e. A ) /\ w e. ( ( nei ` K ) ` { ( F ` y ) } ) ) -> E. v e. ( ( ( nei ` J ) ` { y } ) |`t A ) ( F " v ) C_ w )
49 48 ralrimiva 
 |-  ( ( ph /\ y e. A ) -> A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( ( nei ` J ) ` { y } ) |`t A ) ( F " v ) C_ w )
50 4 adantr 
 |-  ( ( ph /\ y e. A ) -> K e. Haus )
51 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` B ) )
52 51 biimpi 
 |-  ( K e. Top -> K e. ( TopOn ` B ) )
53 50 32 52 3syl 
 |-  ( ( ph /\ y e. A ) -> K e. ( TopOn ` B ) )
54 7 adantr 
 |-  ( ( ph /\ y e. A ) -> ( ( cls ` J ) ` A ) = C )
55 18 54 eleqtrrd 
 |-  ( ( ph /\ y e. A ) -> y e. ( ( cls ` J ) ` A ) )
56 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` C ) )
57 3 56 sylib 
 |-  ( ph -> J e. ( TopOn ` C ) )
58 57 adantr 
 |-  ( ( ph /\ y e. A ) -> J e. ( TopOn ` C ) )
59 6 adantr 
 |-  ( ( ph /\ y e. A ) -> A C_ C )
60 trnei 
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ y e. C ) -> ( y e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { y } ) |`t A ) e. ( Fil ` A ) ) )
61 58 59 18 60 syl3anc 
 |-  ( ( ph /\ y e. A ) -> ( y e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { y } ) |`t A ) e. ( Fil ` A ) ) )
62 55 61 mpbid 
 |-  ( ( ph /\ y e. A ) -> ( ( ( nei ` J ) ` { y } ) |`t A ) e. ( Fil ` A ) )
63 5 adantr 
 |-  ( ( ph /\ y e. A ) -> F : A --> B )
64 flfnei 
 |-  ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { y } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( ( F ` y ) e. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) <-> ( ( F ` y ) e. B /\ A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( ( nei ` J ) ` { y } ) |`t A ) ( F " v ) C_ w ) ) )
65 53 62 63 64 syl3anc 
 |-  ( ( ph /\ y e. A ) -> ( ( F ` y ) e. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) <-> ( ( F ` y ) e. B /\ A. w e. ( ( nei ` K ) ` { ( F ` y ) } ) E. v e. ( ( ( nei ` J ) ` { y } ) |`t A ) ( F " v ) C_ w ) ) )
66 21 49 65 mpbir2and 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) )
67 eleq1w 
 |-  ( x = y -> ( x e. C <-> y e. C ) )
68 67 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
69 sneq 
 |-  ( x = y -> { x } = { y } )
70 69 fveq2d 
 |-  ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
71 70 oveq1d 
 |-  ( x = y -> ( ( ( nei ` J ) ` { x } ) |`t A ) = ( ( ( nei ` J ) ` { y } ) |`t A ) )
72 71 oveq2d 
 |-  ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) )
73 72 fveq1d 
 |-  ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) )
74 73 neeq1d 
 |-  ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) )
75 68 74 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) ) <-> ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) ) )
76 75 8 chvarvv 
 |-  ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) )
77 18 76 syldan 
 |-  ( ( ph /\ y e. A ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) )
78 2 hausflf2 
 |-  ( ( ( K e. Haus /\ ( ( ( nei ` J ) ` { y } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) /\ ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) ~~ 1o )
79 50 62 63 77 78 syl31anc 
 |-  ( ( ph /\ y e. A ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) ~~ 1o )
80 en1eqsn 
 |-  ( ( ( F ` y ) e. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) /\ ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) ~~ 1o ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) = { ( F ` y ) } )
81 66 79 80 syl2anc 
 |-  ( ( ph /\ y e. A ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) = { ( F ` y ) } )
82 81 unieqd 
 |-  ( ( ph /\ y e. A ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) = U. { ( F ` y ) } )
83 fvex 
 |-  ( F ` y ) e. _V
84 83 unisn 
 |-  U. { ( F ` y ) } = ( F ` y )
85 82 84 eqtrdi 
 |-  ( ( ph /\ y e. A ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) = ( F ` y ) )
86 17 20 85 3eqtrd 
 |-  ( ( ph /\ y e. A ) -> ( ( ( ( J CnExt K ) ` F ) |` A ) ` y ) = ( F ` y ) )
87 14 15 86 eqfnfvd 
 |-  ( ph -> ( ( ( J CnExt K ) ` F ) |` A ) = F )