MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnextcn Unicode version

Theorem cnextcn 18051
Description: Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology  J on  C, a subset  A dense in  C, this states a condition for  F from  A to a regular space  K to be extensible by continuity (Contributed by Thierry Arnoux, 1-Jan-2018.)
Hypotheses
Ref Expression
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 )
Assertion
Ref Expression
cnextcn  |-  ( ph  ->  ( ( JCnExt K
) `  F )  e.  ( J  Cn  K
) )
Distinct variable groups:    x, A    x, B    x, C    x, F    x, J    x, K    ph, x

Proof of Theorem cnextcn
Dummy variables  y 
b  d  u  v  z  w  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 731 . . . . 5  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  ph )
2 simpll 731 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  (
w  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  d  e.  ( ( nei `  J
) `  { x } )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )  ->  ph )
3 simpr3 965 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  (
w  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  d  e.  ( ( nei `  J
) `  { x } )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )  -> 
( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )
4 cnextf.3 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  Top )
54ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  (
w  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  d  e.  ( ( nei `  J
) `  { x } )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )  ->  J  e.  Top )
6 simpr2 964 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  (
w  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  d  e.  ( ( nei `  J
) `  { x } )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )  -> 
d  e.  ( ( nei `  J ) `
 { x }
) )
7 neii2 17127 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  d  e.  ( ( nei `  J ) `  { x } ) )  ->  E. v  e.  J  ( {
x }  C_  v  /\  v  C_  d ) )
85, 6, 7syl2anc 643 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  (
w  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  d  e.  ( ( nei `  J
) `  { x } )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )  ->  E. v  e.  J  ( { x }  C_  v  /\  v  C_  d
) )
9 vex 2919 . . . . . . . . . . . . . . . . . . . 20  |-  x  e. 
_V
109snss 3886 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  v  <->  { x }  C_  v )
1110biimpri 198 . . . . . . . . . . . . . . . . . 18  |-  ( { x }  C_  v  ->  x  e.  v )
1211anim1i 552 . . . . . . . . . . . . . . . . 17  |-  ( ( { x }  C_  v  /\  v  C_  d
)  ->  ( x  e.  v  /\  v  C_  d ) )
1312anim2i 553 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) )  ->  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) )
1413anim2i 553 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) ) )  -> 
( ph  /\  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) ) )
1514ex 424 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) ) )
16 3anass 940 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  <->  ( ph  /\  ( v  e.  J  /\  x  e.  v
) ) )
1716anbi1i 677 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ( ph  /\  ( v  e.  J  /\  x  e.  v ) )  /\  v  C_  d ) )
18 anass 631 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
v  e.  J  /\  x  e.  v )
)  /\  v  C_  d )  <->  ( ph  /\  ( ( v  e.  J  /\  x  e.  v )  /\  v  C_  d ) ) )
19 anass 631 . . . . . . . . . . . . . . . . 17  |-  ( ( ( v  e.  J  /\  x  e.  v
)  /\  v  C_  d )  <->  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )
2019anbi2i 676 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
v  e.  J  /\  x  e.  v )  /\  v  C_  d ) )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
2117, 18, 203bitri 263 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
22 opnneip 17138 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  Top  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { x }
) )
234, 22syl3an1 1217 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
2423adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
25 simpr2 964 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  d  /\  ( ph  /\  v  e.  J  /\  x  e.  v ) )  -> 
v  e.  J )
2625ex 424 . . . . . . . . . . . . . . . . 17  |-  ( v 
C_  d  ->  (
( ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  J ) )
2726imdistanri 673 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  J  /\  v  C_  d ) )
2824, 27jca 519 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  ( ( nei `  J ) `
 { x }
)  /\  ( v  e.  J  /\  v  C_  d ) ) )
2921, 28sylbir 205 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) )
3015, 29syl6 31 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) ) )
3130adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) ) )
32 cnextf.4 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  Haus )
33 haustop 17349 . . . . . . . . . . . . . . . . . . . 20  |-  ( K  e.  Haus  ->  K  e. 
Top )
3432, 33syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K  e.  Top )
3534adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  K  e.  Top )
36 imassrn 5175 . . . . . . . . . . . . . . . . . . . 20  |-  ( F
" ( d  i^i 
A ) )  C_  ran  F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : A --> B )
38 frn 5556 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : A --> B  ->  ran  F  C_  B )
3937, 38syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  F  C_  B
)
4036, 39syl5ss 3319 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F " (
d  i^i  A )
)  C_  B )
4140adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( d  i^i 
A ) )  C_  B )
42 ssrin 3526 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  d  ->  (
v  i^i  A )  C_  ( d  i^i  A
) )
43 imass2 5199 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  i^i  A ) 
C_  ( d  i^i 
A )  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
4442, 43syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( v 
C_  d  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
4544adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19  |-  B  = 
U. K
4746clsss 17073 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Top  /\  ( F " ( d  i^i  A ) ) 
C_  B  /\  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )  ->  ( ( cls `  K ) `  ( F " ( v  i^i  A ) ) )  C_  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) ) )
4835, 41, 45, 47syl3anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
49 sstr 3316 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  /\  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5048, 49sylan 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  C_  d )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5150an32s 780 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5251ex 424 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( v  C_  d  ->  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
5352anim2d 549 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( ( v  e.  J  /\  v  C_  d )  ->  (
v  e.  J  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) ) )
5453anim2d 549 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) ) ) )
5531, 54syld 42 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) ) ) )
5655reximdv2 2775 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( E. v  e.  J  ( { x }  C_  v  /\  v  C_  d )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) ( v  e.  J  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) ) )
5756imp 419 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  /\  E. v  e.  J  ( { x }  C_  v  /\  v  C_  d
) )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) ( v  e.  J  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
582, 3, 8, 57syl21anc 1183 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  C )  /\  (
w  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  d  e.  ( ( nei `  J
) `  { x } )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )  ->  E. v  e.  (
( nei `  J
) `  { x } ) ( v  e.  J  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
59583anassrs 1175 . . . . . . 7  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  d  e.  ( ( nei `  J
) `  { x } ) )  /\  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) ( v  e.  J  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
60 simpr 448 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  /\  ( ( cls `  K ) `
 ( F "
u ) )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
61 simp-4l 743 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  /\  ( ( cls `  K ) `
 ( F "
u ) )  C_  w )  ->  ph )
62 simplr 732 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  /\  ( ( cls `  K ) `
 ( F "
u ) )  C_  w )  ->  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )
63 fvex 5701 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { x }
)  e.  _V
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( nei `  J
) `  { x } )  e.  _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17  |-  C  = 
U. J
6665toptopon 16953 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  <->  J  e.  (TopOn `  C ) )
674, 66sylib 189 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  (TopOn `  C ) )
6867elfvexd 5718 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  _V )
69 cnextf.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  C )
7068, 69ssexd 4310 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  _V )
71 elrest 13610 . . . . . . . . . . . . 13  |-  ( ( ( ( nei `  J
) `  { x } )  e.  _V  /\  A  e.  _V )  ->  ( u  e.  ( ( ( nei `  J
) `  { x } )t  A )  <->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) ) )
7264, 70, 71syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  ( ( ( nei `  J
) `  { x } )t  A )  <->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) ) )
7372biimpa 471 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) )
74 imaeq2 5158 . . . . . . . . . . . . . . 15  |-  ( u  =  ( d  i^i 
A )  ->  ( F " u )  =  ( F " (
d  i^i  A )
) )
7574fveq2d 5691 . . . . . . . . . . . . . 14  |-  ( u  =  ( d  i^i 
A )  ->  (
( cls `  K
) `  ( F " u ) )  =  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
7675sseq1d 3335 . . . . . . . . . . . . 13  |-  ( u  =  ( d  i^i 
A )  ->  (
( ( cls `  K
) `  ( F " u ) )  C_  w 
<->  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )
7776biimpcd 216 . . . . . . . . . . . 12  |-  ( ( ( cls `  K
) `  ( F " u ) )  C_  w  ->  ( u  =  ( d  i^i  A
)  ->  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )
)
7877reximdv 2777 . . . . . . . . . . 11  |-  ( ( ( cls `  K
) `  ( F " u ) )  C_  w  ->  ( E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
)  ->  E. d  e.  ( ( nei `  J
) `  { x } ) ( ( cls `  K ) `
 ( F "
( d  i^i  A
) ) )  C_  w ) )
7973, 78syl5 30 . . . . . . . . . 10  |-  ( ( ( cls `  K
) `  ( F " u ) )  C_  w  ->  ( ( ph  /\  u  e.  ( ( ( nei `  J
) `  { x } )t  A ) )  ->  E. d  e.  (
( nei `  J
) `  { x } ) ( ( cls `  K ) `
 ( F "
( d  i^i  A
) ) )  C_  w ) )
8079imp 419 . . . . . . . . 9  |-  ( ( ( ( cls `  K
) `  ( F " u ) )  C_  w  /\  ( ph  /\  u  e.  ( (
( nei `  J
) `  { x } )t  A ) ) )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) ( ( cls `  K ) `
 ( F "
( d  i^i  A
) ) )  C_  w )
8160, 61, 62, 80syl12anc 1182 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  /\  ( ( cls `  K ) `
 ( F "
u ) )  C_  w )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) ( ( cls `  K ) `
 ( F "
( d  i^i  A
) ) )  C_  w )
82 simplll 735 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  ( ph  /\  x  e.  C
) )
83 simplr 732 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
84 cnextf.6 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( cls `  J
) `  A )  =  C )
85 eleq1 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
x  e.  C  <->  y  e.  C ) )
8685anbi2d 685 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  y  e.  C ) ) )
87 sneq 3785 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  { x }  =  { y } )
8887fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { y } ) )
8988oveq1d 6055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { y } )t  A ) )
9089oveq2d 6056 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) )
9190fveq1d 5689 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F ) )
9291neeq1d 2580 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { y } )t  A ) ) `  F )  =/=  (/) ) )
9386, 92imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( 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 )  =/=  (/) ) ) )
94 cnextf.7 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/) )
9593, 94chvarv 2063 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F )  =/=  (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 18049 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
97 fvex 5701 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9897uniex 4664 . . . . . . . . . . . . . . . . 17  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9998snid 3801 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) }
10032adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  Haus )
10184eleq2d 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( x  e.  ( ( cls `  J
) `  A )  <->  x  e.  C ) )
102101biimpar 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  ( ( cls `  J
) `  A )
)
10367adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  J  e.  (TopOn `  C )
)
10469adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  A  C_  C )
105 simpr 448 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  C )
106 trnei 17877 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( J  e.  (TopOn `  C )  /\  A  C_  C  /\  x  e.  C )  ->  (
x  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) ) )
107103, 104, 105, 106syl3anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
x  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) ) )
108102, 107mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) )
10937adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  F : A --> B )
11046hausflf2 17983 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
111100, 108, 109, 94, 110syl31anc 1187 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  ~~  1o )
112 en1b 7134 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) } )
113111, 112sylib 189 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) } )
11499, 113syl5eleqr 2491 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11596, 114eqeltrd 2478 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11646toptopon 16953 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  Top  <->  K  e.  (TopOn `  B ) )
11734, 116sylib 189 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  (TopOn `  B ) )
118117adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  (TopOn `  B )
)
119 flfnei 17976 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  (TopOn `  B )  /\  (
( ( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A )  /\  F : A --> B )  ->  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  <->  ( (
( ( JCnExt K
) `  F ) `  x )  e.  B  /\  A. b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b ) ) )
120118, 108, 109, 119syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  <->  ( (
( ( JCnExt K
) `  F ) `  x )  e.  B  /\  A. b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b ) ) )
121115, 120mpbid 202 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  B  /\  A. b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b ) )
122121simprd 450 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  A. b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b )
123122r19.21bi 2764 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  C )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) ( F " u
)  C_  b )
12482, 83, 123syl2anc 643 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  E. u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) ( F " u
)  C_  b )
12534ad3antrrr 711 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  K  e.  Top )
126 simplr 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
12746neii1 17125 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  e.  ( ( nei `  K ) `  { ( ( ( JCnExt K ) `  F ) `  x
) } ) )  ->  b  C_  B
)
128125, 126, 127syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  C_  B )
129 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
13046clsss 17073 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )
)
131 sstr 3316 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
132130, 131sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u ) 
C_  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
1331323an1rs 1165 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( ( cls `  K
) `  b )  C_  w )  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
134133ex 424 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  C_  B  /\  (
( cls `  K
) `  b )  C_  w )  ->  (
( F " u
)  C_  b  ->  ( ( cls `  K
) `  ( F " u ) )  C_  w ) )
135134reximdv 2777 . . . . . . . . . . . 12  |-  ( ( K  e.  Top  /\  b  C_  B  /\  (
( cls `  K
) `  b )  C_  w )  ->  ( E. u  e.  (
( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b  ->  E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( ( cls `  K ) `
 ( F "
u ) )  C_  w ) )
136125, 128, 129, 135syl3anc 1184 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  ( E. u  e.  (
( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b  ->  E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( ( cls `  K ) `
 ( F "
u ) )  C_  w ) )
137136adantllr 700 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  ( E. u  e.  (
( ( nei `  J
) `  { x } )t  A ) ( F
" u )  C_  b  ->  E. u  e.  ( ( ( nei `  J
) `  { x } )t  A ) ( ( cls `  K ) `
 ( F "
u ) )  C_  w ) )
138124, 137mpd 15 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  E. u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) ( ( cls `  K
) `  ( F " u ) )  C_  w )
13934ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  K  e.  Top )
140 cnextcn.8 . . . . . . . . . . . . . . 15  |-  ( ph  ->  K  e.  Reg )
141140ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  K  e.  Reg )
142141ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  ->  K  e.  Reg )
143 simplr 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  -> 
c  e.  K )
144 simprl 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  -> 
( ( ( JCnExt
K ) `  F
) `  x )  e.  c )
145 regsep 17352 . . . . . . . . . . . . 13  |-  ( ( K  e.  Reg  /\  c  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  c )  ->  E. b  e.  K  ( (
( ( JCnExt K
) `  F ) `  x )  e.  b  /\  ( ( cls `  K ) `  b
)  C_  c )
)
146142, 143, 144, 145syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  ->  E. b  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  c ) )
147 sstr 3316 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  b )  C_  c  /\  c  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
148147expcom 425 . . . . . . . . . . . . . . 15  |-  ( c 
C_  w  ->  (
( ( cls `  K
) `  b )  C_  c  ->  ( ( cls `  K ) `  b )  C_  w
) )
149148anim2d 549 . . . . . . . . . . . . . 14  |-  ( c 
C_  w  ->  (
( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  c )  ->  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  b  /\  (
( cls `  K
) `  b )  C_  w ) ) )
150149reximdv 2777 . . . . . . . . . . . . 13  |-  ( c 
C_  w  ->  ( E. b  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  c )  ->  E. b  e.  K  ( (
( ( JCnExt K
) `  F ) `  x )  e.  b  /\  ( ( cls `  K ) `  b
)  C_  w )
) )
151150ad2antll 710 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  -> 
( E. b  e.  K  ( ( ( ( JCnExt K ) `
 F ) `  x )  e.  b  /\  ( ( cls `  K ) `  b
)  C_  c )  ->  E. b  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  w ) ) )
152146, 151mpd 15 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  ->  E. b  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  w ) )
153 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
154 neii2 17127 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  w  e.  ( ( nei `  K ) `  { ( ( ( JCnExt K ) `  F ) `  x
) } ) )  ->  E. c  e.  K  ( { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c  /\  c  C_  w ) )
155 fvex 5701 . . . . . . . . . . . . . . . . 17  |-  ( ( ( JCnExt K ) `
 F ) `  x )  e.  _V
156155snss 3886 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( JCnExt K
) `  F ) `  x )  e.  c  <->  { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c
)
157156anbi1i 677 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w )  <->  ( {
( ( ( JCnExt
K ) `  F
) `  x ) }  C_  c  /\  c  C_  w ) )
158157biimpri 198 . . . . . . . . . . . . . 14  |-  ( ( { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c  /\  c  C_  w )  ->  ( ( ( ( JCnExt K ) `
 F ) `  x )  e.  c  /\  c  C_  w
) )
159158reximi 2773 . . . . . . . . . . . . 13  |-  ( E. c  e.  K  ( { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c  /\  c  C_  w )  ->  E. c  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  c  /\  c  C_  w ) )
160154, 159syl 16 . . . . . . . . . . . 12  |-  ( ( K  e.  Top  /\  w  e.  ( ( nei `  K ) `  { ( ( ( JCnExt K ) `  F ) `  x
) } ) )  ->  E. c  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  c  /\  c  C_  w ) )
161139, 153, 160syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. c  e.  K  ( (
( ( JCnExt K
) `  F ) `  x )  e.  c  /\  c  C_  w
) )
162152, 161r19.29a 2810 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. b  e.  K  ( (
( ( JCnExt K
) `  F ) `  x )  e.  b  /\  ( ( cls `  K ) `  b
)  C_  w )
)
163 anass 631 . . . . . . . . . . . 12  |-  ( ( ( b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  /\  (
( cls `  K
) `  b )  C_  w )  <->  ( b  e.  K  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  b  /\  (
( cls `  K
) `  b )  C_  w ) ) )
164 opnneip 17138 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Top  /\  b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
1651643expib 1156 . . . . . . . . . . . . 13  |-  ( K  e.  Top  ->  (
( b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) ) )
166165anim1d 548 . . . . . . . . . . . 12  |-  ( K  e.  Top  ->  (
( ( b  e.  K  /\  ( ( ( JCnExt K ) `
 F ) `  x )  e.  b )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  (
b  e.  ( ( nei `  K ) `
 { ( ( ( JCnExt K ) `
 F ) `  x ) } )  /\  ( ( cls `  K ) `  b
)  C_  w )
) )
167163, 166syl5bir 210 . . . . . . . . . . 11  |-  ( K  e.  Top  ->  (
( b  e.  K  /\  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  w ) )  -> 
( b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } )  /\  ( ( cls `  K ) `  b
)  C_  w )
) )
168167reximdv2 2775 . . . . . . . . . 10  |-  ( K  e.  Top  ->  ( E. b  e.  K  ( ( ( ( JCnExt K ) `  F ) `  x
)  e.  b  /\  ( ( cls `  K
) `  b )  C_  w )  ->  E. b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) ( ( cls `  K
) `  b )  C_  w ) )
169139, 162, 168sylc 58 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) ( ( cls `  K
) `  b )  C_  w )
170138, 169r19.29a 2810 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) ( ( cls `  K
) `  ( F " u ) )  C_  w )
17181, 170r19.29a 2810 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) ( ( cls `  K ) `
 ( F "
( d  i^i  A
) ) )  C_  w )
17259, 171r19.29a 2810 . . . . . 6  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) ( v  e.  J  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
173 simplr 732 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
174 simpll 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  ph )
1754ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  J  e.  Top )
176 simplr 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  J )
17765eltopss 16935 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  Top  /\  v  e.  J )  ->  v  C_  C )
178175, 176, 177syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  C_  C )
179 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  v )
180178, 179sseldd 3309 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  C )
181 fvex 5701 . . . . . . . . . . . . . . 15  |-  ( ( nei `  J ) `
 { z } )  e.  _V
182181a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( nei `  J
) `  { z } )  e.  _V )
18370ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  A  e.  _V )
184 opnneip 17138 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { z } ) )
1854, 184syl3an1 1217 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
1861853expa 1153 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
187 elrestr 13611 . . . . . . . . . . . . . 14  |-  ( ( ( ( nei `  J
) `  { z } )  e.  _V  /\  A  e.  _V  /\  v  e.  ( ( nei `  J ) `  { z } ) )  ->  ( v  i^i  A )  e.  ( ( ( nei `  J
) `  { z } )t  A ) )
188182, 183, 186, 187syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )
18965, 46, 4, 32, 37, 69, 84, 94cnextfvval 18049 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  z )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
190189adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( (
( JCnExt K ) `
 F ) `  z )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
19132adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  Haus )
19284eleq2d 2471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( z  e.  ( ( cls `  J
) `  A )  <->  z  e.  C ) )
193192biimpar 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  ( ( cls `  J
) `  A )
)
19467adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  J  e.  (TopOn `  C )
)
19569adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  A  C_  C )
196 simpr 448 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  C )
197 trnei 17877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( J  e.  (TopOn `  C )  /\  A  C_  C  /\  z  e.  C )  ->  (
z  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) ) )
198194, 195, 196, 197syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  (
z  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) ) )
199193, 198mpbid 202 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) )
20037adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  F : A --> B )
201 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  e.  C  <->  z  e.  C ) )
202201anbi2d 685 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  z  e.  C ) ) )
203 sneq 3785 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  { x }  =  { z } )
204203fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { z } ) )
205204oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
206205oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) )
207206fveq1d 5689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
208207neeq1d 2580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =/=  (/) ) )
209202, 208imbi12d 312 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
( ( ph  /\  x  e.  C )  ->  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/) )  <->  ( ( ph  /\  z  e.  C
)  ->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =/=  (/) ) ) )
210209, 94chvarv 2063 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =/=  (/) )
21146hausflf2 17983 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  e.  Haus  /\  ( ( ( nei `  J ) `  {
z } )t  A )  e.  ( Fil `  A
)  /\  F : A
--> B )  /\  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =/=  (/) )  -> 
( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o )
212191, 199, 200, 210, 211syl31anc 1187 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o )
213 en1b 7134 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o  <->  ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) } )
214212, 213sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) } )
215214adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) } )
216117adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  (TopOn `  B )
)
217 flfval 17975 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  (TopOn `  B )  /\  (
( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A )  /\  F : A --> B )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J ) `  {
z } )t  A ) ) ) )
218216, 199, 200, 217syl3anc 1184 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J ) `  {
z } )t  A ) ) ) )
219218adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J ) `  {
z } )t  A ) ) ) )
220 uniexg 4665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( K  e.  Haus  ->  U. K  e.  _V )
22132, 220syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U. K  e.  _V )
222221ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  U. K  e. 
_V )
22346, 222syl5eqel 2488 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  B  e.  _V )
224199adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( (
( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) )
225 filfbas 17833 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A )  ->  ( ( ( nei `  J ) `
 { z } )t  A )  e.  (
fBas `  A )
)
226224, 225syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( (
( nei `  J
) `  { z } )t  A )  e.  (
fBas `  A )
)
22737ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  F : A
--> B )
228 simpr 448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( v  i^i  A )  e.  ( ( ( nei `  J
) `  { z } )t  A ) )
229 fgfil 17860 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A )  ->  ( A filGen ( ( ( nei `  J
) `  { z } )t  A ) )  =  ( ( ( nei `  J ) `  {
z } )t  A ) )
230199, 229syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  ( A filGen ( ( ( nei `  J ) `
 { z } )t  A ) )  =  ( ( ( nei `  J ) `  {
z } )t  A ) )
231230adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( A filGen ( ( ( nei `  J ) `  {
z } )t  A ) )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
232228, 231eleqtrrd 2481 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( v  i^i  A )  e.  ( A filGen ( ( ( nei `  J ) `
 { z } )t  A ) ) )
233 eqid 2404 . . . . . . . . . . . . . . . . . . . 20  |-  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )  =  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )
234233imaelfm 17936 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( B  e.  _V  /\  ( ( ( nei `  J ) `  {
z } )t  A )  e.  ( fBas `  A
)  /\  F : A
--> B )  /\  (
v  i^i  A )  e.  ( A filGen ( ( ( nei `  J
) `  { z } )t  A ) ) )  ->  ( F "
( v  i^i  A
) )  e.  ( ( B  FilMap  F ) `
 ( ( ( nei `  J ) `
 { z } )t  A ) ) )
235223, 226, 227, 232, 234syl31anc 1187 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( F " ( v  i^i  A
) )  e.  ( ( B  FilMap  F ) `
 ( ( ( nei `  J ) `
 { z } )t  A ) ) )
236 flimclsi 17963 . . . . . . . . . . . . . . . . . 18  |-  ( ( F " ( v  i^i  A ) )  e.  ( ( B 
FilMap  F ) `  (
( ( nei `  J
) `  { z } )t  A ) )  -> 
( K  fLim  (
( B  FilMap  F ) `
 ( ( ( nei `  J ) `
 { z } )t  A ) ) ) 
C_  ( ( cls `  K ) `  ( F " ( v  i^i 
A ) ) ) )
237235, 236syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J
) `  { z } )t  A ) ) ) 
C_  ( ( cls `  K ) `  ( F " ( v  i^i 
A ) ) ) )
238219, 237eqsstrd 3342 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  C_  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
239215, 238eqsstr3d 3343 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  { U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) }  C_  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
240 fvex 5701 . . . . . . . . . . . . . . . . 17  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
241240uniex 4664 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
242241snss 3886 . . . . . . . . . . . . . . 15  |-  ( U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  <->  { U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) }  C_  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
243239, 242sylibr 204 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
244190, 243eqeltrd 2478 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( (
( JCnExt K ) `
 F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
245174, 180, 188, 244syl21anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
246245adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
247173, 246sseldd 3309 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  w
)
248247ralrimiva 2749 . . . . . . . . 9  |-  ( ( ( ph  /\  v  e.  J )  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  ->  A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
)
249248expl 602 . . . . . . . 8  |-  ( ph  ->  ( ( v  e.  J  /\  ( ( cls `  K ) `
 ( F "
( v  i^i  A
) ) )  C_  w )  ->  A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
250249reximdv 2777 . . . . . . 7  |-  ( ph  ->  ( E. v  e.  ( ( nei `  J
) `  { x } ) ( v  e.  J  /\  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
251250ad2antrr 707 . . . . . 6  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  ( E. v  e.  ( ( nei `  J ) `  { x } ) ( v  e.  J  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
252172, 251mpd 15 . . . . 5  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
)
25365, 46, 4, 32, 37, 69, 84, 94cnextf 18050 . . . . . . . . . 10  |-  ( ph  ->  ( ( JCnExt K
) `  F ) : C --> B )
254 ffun 5552 . . . . . . . . . 10  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  Fun  ( ( JCnExt K
) `  F )
)
255253, 254syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  ( ( JCnExt
K ) `  F
) )
256255adantr 452 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  Fun  ( ( JCnExt K
) `  F )
)
25765neii1 17125 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  v  e.  ( ( nei `  J ) `  { x } ) )  ->  v  C_  C )
2584, 257sylan 458 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  C )
259 fdm 5554 . . . . . . . . . . 11  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  dom  ( ( JCnExt K
) `  F )  =  C )
260253, 259syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( JCnExt
K ) `  F
)  =  C )
261260adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  dom  ( ( JCnExt K
) `  F )  =  C )
262258, 261sseqtr4d 3345 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  dom  ( ( JCnExt K ) `  F ) )
263 funimass4 5736 . . . . . . . 8  |-  ( ( Fun  ( ( JCnExt
K ) `  F
)  /\  v  C_  dom  ( ( JCnExt K
) `  F )
)  ->  ( (
( ( JCnExt K
) `  F ) " v )  C_  w 
<-> 
A. z  e.  v  ( ( ( JCnExt
K ) `  F
) `  z )  e.  w ) )
264256, 262, 263syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( ( ( JCnExt K ) `  F ) " v
)  C_  w  <->  A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
265264biimprd 215 . . . . . 6  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( A. z  e.  v  ( ( ( JCnExt K ) `  F ) `  z
)  e.  w  -> 
( ( ( JCnExt
K ) `  F
) " v ) 
C_  w ) )
266265reximdva 2778 . . . . 5  |-  ( ph  ->  ( E. v  e.  ( ( nei `  J
) `  { x } ) A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w  ->  E. v  e.  ( ( nei `  J
) `  { x } ) ( ( ( JCnExt K ) `
 F ) "
v )  C_  w
) )
2671, 252, 266sylc 58 . . . 4  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  E. v  e.  ( ( nei `  J
) `  { x } ) ( ( ( JCnExt K ) `
 F ) "
v )  C_  w
)
268267ralrimiva 2749 . . 3  |-  ( (
ph  /\  x  e.  C )  ->  A. w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. v  e.  ( ( nei `  J
) `  { x } ) ( ( ( JCnExt K ) `
 F ) "
v )  C_  w
)
269268ralrimiva 2749 . 2  |-  ( ph  ->  A. x  e.  C  A. w  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. v  e.  ( ( nei `  J
) `  { x } ) ( ( ( JCnExt K ) `
 F ) "
v )  C_  w
)
27065, 46cnnei 17300 . . 3  |-  ( ( J  e.  Top  /\  K  e.  Top  /\  (
( JCnExt K ) `
 F ) : C --> B )  -> 
( ( ( JCnExt
K ) `  F
)  e.  ( J  Cn  K )  <->  A. x  e.  C  A. w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. v  e.  ( ( nei `  J
) `  { x } ) ( ( ( JCnExt K ) `
 F ) "
v )  C_  w
) )
2714, 34, 253, 270syl3anc 1184 . 2  |-  ( ph  ->  ( ( ( JCnExt
K ) `  F
)  e.  ( J  Cn  K )  <->  A. x  e.  C  A. w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) E. v  e.  ( ( nei `  J
) `  { x } ) ( ( ( JCnExt K ) `
 F ) "
v )  C_  w
) )
272269, 271mpbird 224 1  |-  ( ph  ->  ( ( JCnExt K
) `  F )  e.  ( J  Cn  K
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916    i^i cin 3279    C_ wss 3280   (/)c0 3588   {csn 3774   U.cuni 3975   class class class wbr 4172   dom cdm 4837   ran crn 4838   "cima 4840   Fun wfun 5407   -->wf 5409   ` cfv 5413  (class class class)co 6040   1oc1o 6676    ~~ cen 7065   ↾t crest 13603   fBascfbas 16644   filGencfg 16645   Topctop 16913  TopOnctopon 16914   clsccl 17037   neicnei 17116    Cn ccn 17242   Hauscha 17326   Regcreg 17327   Filcfil 17830    FilMap cfm 17918    fLim cflim 17919    fLimf cflf 17920  CnExtccnext 18043
This theorem is referenced by:  cnextucn  18286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-suc 4547  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-1o 6683  df-map 6979  df-pm 6980  df-en 7069  df-rest 13605  df-topgen 13622  df-fbas 16654  df-fg 16655  df-top 16918  df-topon 16921  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-cn 17245  df-cnp 17246  df-haus 17333  df-reg 17334  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-cnext 18044
  Copyright terms: Public domain W3C validator