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 = 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 ) =/= (/) )
Assertion cnextfvval 
|- ( ( ph /\ X e. C ) -> ( ( ( J CnExt K ) ` F ) ` X ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t 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 3 adantr 
 |-  ( ( ph /\ X e. C ) -> J e. Top )
10 4 adantr 
 |-  ( ( ph /\ X e. C ) -> K e. Haus )
11 5 adantr 
 |-  ( ( ph /\ X e. C ) -> F : A --> B )
12 6 adantr 
 |-  ( ( ph /\ X e. C ) -> A C_ C )
13 1 2 cnextfun 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) )
14 9 10 11 12 13 syl22anc 
 |-  ( ( ph /\ X e. C ) -> Fun ( ( J CnExt K ) ` F ) )
15 7 eleq2d 
 |-  ( ph -> ( X e. ( ( cls ` J ) ` A ) <-> X e. C ) )
16 15 biimpar 
 |-  ( ( ph /\ X e. C ) -> X e. ( ( cls ` J ) ` A ) )
17 fvex 
 |-  ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. _V
18 17 uniex 
 |-  U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. _V
19 18 snid 
 |-  U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t 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 } ) |`t A ) = ( ( ( nei ` J ) ` { X } ) |`t A ) )
23 22 oveq2d 
 |-  ( x = X -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) )
24 23 fveq1d 
 |-  ( x = X -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
25 24 breq1d 
 |-  ( x = X -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o <-> ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ~~ 1o ) )
26 25 imbi2d 
 |-  ( x = X -> ( ( ph -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o ) <-> ( ph -> ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ~~ 1o ) ) )
27 4 adantr 
 |-  ( ( ph /\ x e. C ) -> K e. Haus )
28 3 adantr 
 |-  ( ( ph /\ x e. C ) -> J e. Top )
29 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` C ) )
30 28 29 sylib 
 |-  ( ( ph /\ x e. C ) -> J e. ( TopOn ` C ) )
31 6 adantr 
 |-  ( ( ph /\ x e. C ) -> A C_ C )
32 simpr 
 |-  ( ( ph /\ x e. C ) -> x e. C )
33 7 eleq2d 
 |-  ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
34 33 biimpar 
 |-  ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
35 trnei 
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
36 35 biimpa 
 |-  ( ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
37 30 31 32 34 36 syl31anc 
 |-  ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
38 5 adantr 
 |-  ( ( ph /\ x e. C ) -> F : A --> B )
39 2 hausflf2 
 |-  ( ( ( K e. Haus /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) /\ ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o )
40 27 37 38 8 39 syl31anc 
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o )
41 40 expcom 
 |-  ( x e. C -> ( ph -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o ) )
42 26 41 vtoclga 
 |-  ( X e. C -> ( ph -> ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ~~ 1o ) )
43 42 impcom 
 |-  ( ( ph /\ X e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ~~ 1o )
44 en1b 
 |-  ( ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ~~ 1o <-> ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) } )
45 43 44 sylib 
 |-  ( ( ph /\ X e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) } )
46 19 45 eleqtrrid 
 |-  ( ( ph /\ X e. C ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
47 nfiu1 
 |-  F/_ x U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
48 47 nfel2 
 |-  F/ x <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
49 nfv 
 |-  F/ x ( X e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
50 48 49 nfbi 
 |-  F/ x ( <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( X e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
51 opeq1 
 |-  ( x = X -> <. x , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. = <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. )
52 51 eleq1d 
 |-  ( x = X -> ( <. x , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
53 eleq1 
 |-  ( x = X -> ( x e. ( ( cls ` J ) ` A ) <-> X e. ( ( cls ` J ) ` A ) ) )
54 24 eleq2d 
 |-  ( x = X -> ( U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) <-> U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
55 53 54 anbi12d 
 |-  ( x = X -> ( ( x e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( X e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) ) )
56 52 55 bibi12d 
 |-  ( x = X -> ( ( <. x , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) <-> ( <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( X e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) ) ) )
57 opeliunxp 
 |-  ( <. x , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
58 50 56 57 vtoclg1f 
 |-  ( X e. C -> ( <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( X e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) ) )
59 58 adantl 
 |-  ( ( ph /\ X e. C ) -> ( <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( X e. ( ( cls ` J ) ` A ) /\ U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) ) )
60 16 46 59 mpbir2and 
 |-  ( ( ph /\ X e. C ) -> <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
61 df-br 
 |-  ( X ( ( J CnExt K ) ` F ) U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) <-> <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. ( ( J CnExt K ) ` F ) )
62 haustop 
 |-  ( K e. Haus -> K e. Top )
63 4 62 syl 
 |-  ( ph -> K e. Top )
64 63 adantr 
 |-  ( ( ph /\ X e. C ) -> K e. Top )
65 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 ) ) )
66 9 64 11 12 65 syl22anc 
 |-  ( ( ph /\ X e. C ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
67 66 eleq2d 
 |-  ( ( ph /\ X e. C ) -> ( <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. ( ( J CnExt K ) ` F ) <-> <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
68 61 67 syl5bb 
 |-  ( ( ph /\ X e. C ) -> ( X ( ( J CnExt K ) ` F ) U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) <-> <. X , U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
69 60 68 mpbird 
 |-  ( ( ph /\ X e. C ) -> X ( ( J CnExt K ) ` F ) U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
70 funbrfv 
 |-  ( Fun ( ( J CnExt K ) ` F ) -> ( X ( ( J CnExt K ) ` F ) U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) -> ( ( ( J CnExt K ) ` F ) ` X ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
71 14 69 70 sylc 
 |-  ( ( ph /\ X e. C ) -> ( ( ( J CnExt K ) ` F ) ` X ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )