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

Theorem cnextcn 19651
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 753 . . . . 5  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  ph )
2 simpll 753 . . . . . . . . 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 996 . . . . . . . . 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 725 . . . . . . . . . 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 995 . . . . . . . . . 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 18724 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  d  e.  ( ( nei `  J ) `  { x } ) )  ->  E. v  e.  J  ( {
x }  C_  v  /\  v  C_  d ) )
85, 6, 7syl2anc 661 . . . . . . . . 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 2987 . . . . . . . . . . . . . . . . . . . 20  |-  x  e. 
_V
109snss 4011 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  v  <->  { x }  C_  v )
1110biimpri 206 . . . . . . . . . . . . . . . . . 18  |-  ( { x }  C_  v  ->  x  e.  v )
1211anim1i 568 . . . . . . . . . . . . . . . . 17  |-  ( ( { x }  C_  v  /\  v  C_  d
)  ->  ( x  e.  v  /\  v  C_  d ) )
1312anim2i 569 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) )  ->  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) )
1413anim2i 569 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) ) )  -> 
( ph  /\  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) ) )
1514ex 434 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) ) )
16 3anass 969 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  <->  ( ph  /\  ( v  e.  J  /\  x  e.  v
) ) )
1716anbi1i 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ( ph  /\  ( v  e.  J  /\  x  e.  v ) )  /\  v  C_  d ) )
18 anass 649 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
v  e.  J  /\  x  e.  v )
)  /\  v  C_  d )  <->  ( ph  /\  ( ( v  e.  J  /\  x  e.  v )  /\  v  C_  d ) ) )
19 anass 649 . . . . . . . . . . . . . . . . 17  |-  ( ( ( v  e.  J  /\  x  e.  v
)  /\  v  C_  d )  <->  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )
2019anbi2i 694 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
v  e.  J  /\  x  e.  v )  /\  v  C_  d ) )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
2117, 18, 203bitri 271 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
22 opnneip 18735 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  Top  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { x }
) )
234, 22syl3an1 1251 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
2423adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
25 simpr2 995 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  d  /\  ( ph  /\  v  e.  J  /\  x  e.  v ) )  -> 
v  e.  J )
2625ex 434 . . . . . . . . . . . . . . . . 17  |-  ( v 
C_  d  ->  (
( ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  J ) )
2726imdistanri 691 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  J  /\  v  C_  d ) )
2824, 27jca 532 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  ( ( nei `  J ) `
 { x }
)  /\  ( v  e.  J  /\  v  C_  d ) ) )
2921, 28sylbir 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) )
3015, 29syl6 33 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) ) )
3130adantr 465 . . . . . . . . . . . 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 18947 . . . . . . . . . . . . . . . . . . . 20  |-  ( K  e.  Haus  ->  K  e. 
Top )
3432, 33syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K  e.  Top )
3534adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  K  e.  Top )
36 imassrn 5192 . . . . . . . . . . . . . . . . . . . 20  |-  ( F
" ( d  i^i 
A ) )  C_  ran  F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : A --> B )
38 frn 5577 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : A --> B  ->  ran  F  C_  B )
3937, 38syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  F  C_  B
)
4036, 39syl5ss 3379 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F " (
d  i^i  A )
)  C_  B )
4140adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( d  i^i 
A ) )  C_  B )
42 ssrin 3587 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  d  ->  (
v  i^i  A )  C_  ( d  i^i  A
) )
43 imass2 5216 . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19  |-  B  = 
U. K
4746clsss 18670 . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
49 sstr 3376 . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  C_  d )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5150an32s 802 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5251ex 434 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( v  C_  d  ->  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
5352anim2d 565 . . . . . . . . . . . . 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 565 . . . . . . . . . . . 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 44 . . . . . . . . . . 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 2837 . . . . . . . . . 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 429 . . . . . . . . 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 1217 . . . . . . . 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 1209 . . . . . . 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 461 . . . . . . . . 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 765 . . . . . . . . 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 754 . . . . . . . . 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 5713 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { x }
)  e.  _V
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( nei `  J
) `  { x } )  e.  _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17  |-  C  = 
U. J
6665toptopon 18550 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  <->  J  e.  (TopOn `  C ) )
674, 66sylib 196 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  (TopOn `  C ) )
6867elfvexd 5730 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  _V )
69 cnextf.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  C )
7068, 69ssexd 4451 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  _V )
71 elrest 14378 . . . . . . . . . . . . 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 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  ( ( ( nei `  J
) `  { x } )t  A )  <->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) ) )
7372biimpa 484 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) )
74 imaeq2 5177 . . . . . . . . . . . . . . 15  |-  ( u  =  ( d  i^i 
A )  ->  ( F " u )  =  ( F " (
d  i^i  A )
) )
7574fveq2d 5707 . . . . . . . . . . . . . 14  |-  ( u  =  ( d  i^i 
A )  ->  (
( cls `  K
) `  ( F " u ) )  =  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
7675sseq1d 3395 . . . . . . . . . . . . 13  |-  ( u  =  ( d  i^i 
A )  ->  (
( ( cls `  K
) `  ( F " u ) )  C_  w 
<->  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )
7776biimpcd 224 . . . . . . . . . . . 12  |-  ( ( ( cls `  K
) `  ( F " u ) )  C_  w  ->  ( u  =  ( d  i^i  A
)  ->  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )
)
7877reximdv 2839 . . . . . . . . . . 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 32 . . . . . . . . . 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 429 . . . . . . . . 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 1216 . . . . . . . 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 757 . . . . . . . . . . 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 754 . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
x  e.  C  <->  y  e.  C ) )
8685anbi2d 703 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  y  e.  C ) ) )
87 sneq 3899 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  { x }  =  { y } )
8887fveq2d 5707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { y } ) )
8988oveq1d 6118 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { y } )t  A ) )
9089oveq2d 6119 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) )
9190fveq1d 5705 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F ) )
9291neeq1d 2633 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { y } )t  A ) ) `  F )  =/=  (/) ) )
9386, 92imbi12d 320 . . . . . . . . . . . . . . . . 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 1958 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F )  =/=  (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 19649 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
97 fvex 5713 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9897uniex 6388 . . . . . . . . . . . . . . . . 17  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9998snid 3917 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) }
10032adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  Haus )
10184eleq2d 2510 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( x  e.  ( ( cls `  J
) `  A )  <->  x  e.  C ) )
102101biimpar 485 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  ( ( cls `  J
) `  A )
)
10367adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  J  e.  (TopOn `  C )
)
10469adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  A  C_  C )
105 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  C )
106 trnei 19477 . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
x  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) ) )
108102, 107mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) )
10937adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  F : A --> B )
11046hausflf2 19583 . . . . . . . . . . . . . . . . . 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 1221 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  ~~  1o )
112 en1b 7389 . . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) } )
11499, 113syl5eleqr 2530 . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11646toptopon 18550 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  Top  <->  K  e.  (TopOn `  B ) )
11734, 116sylib 196 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  (TopOn `  B ) )
118117adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  (TopOn `  B )
)
119 flfnei 19576 . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 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 463 . . . . . . . . . . . 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 2826 . . . . . . . . . . 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 661 . . . . . . . . . 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 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  K  e.  Top )
126 simplr 754 . . . . . . . . . . . . 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 18722 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  e.  ( ( nei `  K ) `  { ( ( ( JCnExt K ) `  F ) `  x
) } ) )  ->  b  C_  B
)
128125, 126, 127syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  C_  B )
129 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
13046clsss 18670 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )
)
131 sstr 3376 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
132130, 131sylan 471 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u ) 
C_  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
1331323an1rs 1199 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( ( cls `  K
) `  b )  C_  w )  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
134133ex 434 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  C_  B  /\  (
( cls `  K
) `  b )  C_  w )  ->  (
( F " u
)  C_  b  ->  ( ( cls `  K
) `  ( F " u ) )  C_  w ) )
135134reximdv 2839 . . . . . . . . . . . 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 1218 . . . . . . . . . . 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 718 . . . . . . . . . 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 725 . . . . . . . . . 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 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  K  e.  Reg )
142141ad2antrr 725 . . . . . . . . . . . . 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 754 . . . . . . . . . . . . 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 755 . . . . . . . . . . . . 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 18950 . . . . . . . . . . . . 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 1218 . . . . . . . . . . . 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 3376 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  b )  C_  c  /\  c  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
148147expcom 435 . . . . . . . . . . . . . . 15  |-  ( c 
C_  w  ->  (
( ( cls `  K
) `  b )  C_  c  ->  ( ( cls `  K ) `  b )  C_  w
) )
149148anim2d 565 . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . 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 728 . . . . . . . . . . . 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 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
154 neii2 18724 . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . 17  |-  ( ( ( JCnExt K ) `
 F ) `  x )  e.  _V
156155snss 4011 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( JCnExt K
) `  F ) `  x )  e.  c  <->  { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c
)
157156anbi1i 695 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w )  <->  ( {
( ( ( JCnExt
K ) `  F
) `  x ) }  C_  c  /\  c  C_  w ) )
158157biimpri 206 . . . . . . . . . . . . . 14  |-  ( ( { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c  /\  c  C_  w )  ->  ( ( ( ( JCnExt K ) `
 F ) `  x )  e.  c  /\  c  C_  w
) )
159158reximi 2835 . . . . . . . . . . . . 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 661 . . . . . . . . . . 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 2874 . . . . . . . . . 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 649 . . . . . . . . . . . 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 18735 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Top  /\  b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
1651643expib 1190 . . . . . . . . . . . . 13  |-  ( K  e.  Top  ->  (
( b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) ) )
166165anim1d 564 . . . . . . . . . . . 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 218 . . . . . . . . . . 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 2837 . . . . . . . . . 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 60 . . . . . . . . 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 2874 . . . . . . . 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 2874 . . . . . . 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 2874 . . . . . 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 754 . . . . . . . . . . 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 753 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  ph )
1754ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  J  e.  Top )
176 simplr 754 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  J )
17765eltopss 18532 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  Top  /\  v  e.  J )  ->  v  C_  C )
178175, 176, 177syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  C_  C )
179 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  v )
180178, 179sseldd 3369 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  C )
181 fvex 5713 . . . . . . . . . . . . . . 15  |-  ( ( nei `  J ) `
 { z } )  e.  _V
182181a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( nei `  J
) `  { z } )  e.  _V )
18370ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  A  e.  _V )
184 opnneip 18735 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { z } ) )
1854, 184syl3an1 1251 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
1861853expa 1187 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
187 elrestr 14379 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 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 19649 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  z )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
190189adantr 465 . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  Haus )
19284eleq2d 2510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( z  e.  ( ( cls `  J
) `  A )  <->  z  e.  C ) )
193192biimpar 485 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  ( ( cls `  J
) `  A )
)
19467adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  J  e.  (TopOn `  C )
)
19569adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  A  C_  C )
196 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  C )
197 trnei 19477 . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  (
z  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) ) )
199193, 198mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) )
20037adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  F : A --> B )
201 eleq1 2503 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  e.  C  <->  z  e.  C ) )
202201anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  z  e.  C ) ) )
203 sneq 3899 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  { x }  =  { z } )
204203fveq2d 5707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { z } ) )
205204oveq1d 6118 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
206205oveq2d 6119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) )
207206fveq1d 5705 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
208207neeq1d 2633 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =/=  (/) ) )
209202, 208imbi12d 320 . . . . . . . . . . . . . . . . . . . 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 1958 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =/=  (/) )
21146hausflf2 19583 . . . . . . . . . . . . . . . . . . 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 1221 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o )
213 en1b 7389 . . . . . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) } )
215214adantr 465 . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  (TopOn `  B )
)
217 flfval 19575 . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J ) `  {
z } )t  A ) ) ) )
219218adantr 465 . . . . . . . . . . . . . . . . 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 6389 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( K  e.  Haus  ->  U. K  e.  _V )
22132, 220syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U. K  e.  _V )
222221ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  U. K  e. 
_V )
22346, 222syl5eqel 2527 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  B  e.  _V )
224199adantr 465 . . . . . . . . . . . . . . . . . . . 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 19433 . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  F : A
--> B )
228 simpr 461 . . . . . . . . . . . . . . . . . . . 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 19460 . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . 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 2520 . . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . . . . 20  |-  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )  =  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )
234233imaelfm 19536 . . . . . . . . . . . . . . . . . . 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 1221 . . . . . . . . . . . . . . . . . 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 19563 . . . . . . . . . . . . . . . . . 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 3402 . . . . . . . . . . . . . . . 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 3403 . . . . . . . . . . . . . . 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 5713 . . . . . . . . . . . . . . . . 17  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
241240uniex 6388 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
242241snss 4011 . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . 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 1217 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
246245adantlr 714 . . . . . . . . . . 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 3369 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  w
)
248247ralrimiva 2811 . . . . . . . . 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 618 . . . . . . . 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 2839 . . . . . . 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 725 . . . . . 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 19650 . . . . . . . . . 10  |-  ( ph  ->  ( ( JCnExt K
) `  F ) : C --> B )
254 ffun 5573 . . . . . . . . . 10  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  Fun  ( ( JCnExt K
) `  F )
)
255253, 254syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  ( ( JCnExt
K ) `  F
) )
256255adantr 465 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  Fun  ( ( JCnExt K
) `  F )
)
25765neii1 18722 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  v  e.  ( ( nei `  J ) `  { x } ) )  ->  v  C_  C )
2584, 257sylan 471 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  C )
259 fdm 5575 . . . . . . . . . . 11  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  dom  ( ( JCnExt K
) `  F )  =  C )
260253, 259syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( JCnExt
K ) `  F
)  =  C )
261260adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  dom  ( ( JCnExt K
) `  F )  =  C )
262258, 261sseqtr4d 3405 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  dom  ( ( JCnExt K ) `  F ) )
263 funimass4 5754 . . . . . . . 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 661 . . . . . . 7  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( ( ( JCnExt K ) `  F ) " v
)  C_  w  <->  A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
265264biimprd 223 . . . . . 6  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( A. z  e.  v  ( ( ( JCnExt K ) `  F ) `  z
)  e.  w  -> 
( ( ( JCnExt
K ) `  F
) " v ) 
C_  w ) )
266265reximdva 2840 . . . . 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 60 . . . 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 2811 . . 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 2811 . 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 18898 . . 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 1218 . 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 232 1  |-  ( ph  ->  ( ( JCnExt K
) `  F )  e.  ( J  Cn  K
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756    =/= wne 2618   A.wral 2727   E.wrex 2728   _Vcvv 2984    i^i cin 3339    C_ wss 3340   (/)c0 3649   {csn 3889   U.cuni 4103   class class class wbr 4304   dom cdm 4852   ran crn 4853   "cima 4855   Fun wfun 5424   -->wf 5426   ` cfv 5430  (class class class)co 6103   1oc1o 6925    ~~ cen 7319   ↾t crest 14371   fBascfbas 17816   filGencfg 17817   Topctop 18510  TopOnctopon 18511   clsccl 18634   neicnei 18713    Cn ccn 18840   Hauscha 18924   Regcreg 18925   Filcfil 19430    FilMap cfm 19518    fLim cflim 19519    fLimf cflf 19520  CnExtccnext 19643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-int 4141  df-iun 4185  df-iin 4186  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-1st 6589  df-2nd 6590  df-1o 6932  df-map 7228  df-pm 7229  df-en 7323  df-rest 14373  df-topgen 14394  df-fbas 17826  df-fg 17827  df-top 18515  df-topon 18518  df-cld 18635  df-ntr 18636  df-cls 18637  df-nei 18714  df-cn 18843  df-cnp 18844  df-haus 18931  df-reg 18932  df-fil 19431  df-fm 19523  df-flim 19524  df-flf 19525  df-cnext 19644
This theorem is referenced by:  cnextucn  19890
  Copyright terms: Public domain W3C validator