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

Theorem cnextcn 21160
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 768 . . . . 5  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  ph )
2 simpll 768 . . . . . . . . 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 1038 . . . . . . . . 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 740 . . . . . . . . . 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 1037 . . . . . . . . . 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 20201 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  d  e.  ( ( nei `  J ) `  { x } ) )  ->  E. v  e.  J  ( {
x }  C_  v  /\  v  C_  d ) )
85, 6, 7syl2anc 673 . . . . . . . . 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 3034 . . . . . . . . . . . . . . . . . . . 20  |-  x  e. 
_V
109snss 4087 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  v  <->  { x }  C_  v )
1110biimpri 211 . . . . . . . . . . . . . . . . . 18  |-  ( { x }  C_  v  ->  x  e.  v )
1211anim1i 578 . . . . . . . . . . . . . . . . 17  |-  ( ( { x }  C_  v  /\  v  C_  d
)  ->  ( x  e.  v  /\  v  C_  d ) )
1312anim2i 579 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) )  ->  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) )
1413anim2i 579 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) ) )  -> 
( ph  /\  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) ) )
1514ex 441 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) ) )
16 3anass 1011 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  <->  ( ph  /\  ( v  e.  J  /\  x  e.  v
) ) )
1716anbi1i 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ( ph  /\  ( v  e.  J  /\  x  e.  v ) )  /\  v  C_  d ) )
18 anass 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
v  e.  J  /\  x  e.  v )
)  /\  v  C_  d )  <->  ( ph  /\  ( ( v  e.  J  /\  x  e.  v )  /\  v  C_  d ) ) )
19 anass 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( v  e.  J  /\  x  e.  v
)  /\  v  C_  d )  <->  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )
2019anbi2i 708 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
v  e.  J  /\  x  e.  v )  /\  v  C_  d ) )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
2117, 18, 203bitri 279 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
22 opnneip 20212 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  Top  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { x }
) )
234, 22syl3an1 1325 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
2423adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
25 simpr2 1037 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  d  /\  ( ph  /\  v  e.  J  /\  x  e.  v ) )  -> 
v  e.  J )
2625ex 441 . . . . . . . . . . . . . . . . 17  |-  ( v 
C_  d  ->  (
( ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  J ) )
2726imdistanri 705 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  J  /\  v  C_  d ) )
2824, 27jca 541 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  ( ( nei `  J ) `
 { x }
)  /\  ( v  e.  J  /\  v  C_  d ) ) )
2921, 28sylbir 218 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . 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 20424 . . . . . . . . . . . . . . . . . . . 20  |-  ( K  e.  Haus  ->  K  e. 
Top )
3432, 33syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K  e.  Top )
3534adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  K  e.  Top )
36 imassrn 5185 . . . . . . . . . . . . . . . . . . . 20  |-  ( F
" ( d  i^i 
A ) )  C_  ran  F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : A --> B )
38 frn 5747 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : A --> B  ->  ran  F  C_  B )
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  F  C_  B
)
4036, 39syl5ss 3429 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F " (
d  i^i  A )
)  C_  B )
4140adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( d  i^i 
A ) )  C_  B )
42 ssrin 3648 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  d  ->  (
v  i^i  A )  C_  ( d  i^i  A
) )
43 imass2 5210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  i^i  A ) 
C_  ( d  i^i 
A )  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( v 
C_  d  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
4544adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19  |-  B  = 
U. K
4746clsss 20146 . . . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
49 sstr 3426 . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  C_  d )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5150an32s 821 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5251ex 441 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( v  C_  d  ->  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
5352anim2d 575 . . . . . . . . . . . . 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 575 . . . . . . . . . . . 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 2855 . . . . . . . . . 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 436 . . . . . . . . 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 1291 . . . . . . . 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 1256 . . . . . . 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 468 . . . . . . . . 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 784 . . . . . . . . 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 770 . . . . . . . . 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 5889 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { x }
)  e.  _V
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( nei `  J
) `  { x } )  e.  _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17  |-  C  = 
U. J
6665toptopon 20025 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  <->  J  e.  (TopOn `  C ) )
674, 66sylib 201 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  (TopOn `  C ) )
6867elfvexd 5907 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  _V )
69 cnextf.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  C )
7068, 69ssexd 4543 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  _V )
71 elrest 15404 . . . . . . . . . . . . 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 673 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  ( ( ( nei `  J
) `  { x } )t  A )  <->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) ) )
7372biimpa 492 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) )
74 imaeq2 5170 . . . . . . . . . . . . . . 15  |-  ( u  =  ( d  i^i 
A )  ->  ( F " u )  =  ( F " (
d  i^i  A )
) )
7574fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( u  =  ( d  i^i 
A )  ->  (
( cls `  K
) `  ( F " u ) )  =  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
7675sseq1d 3445 . . . . . . . . . . . . 13  |-  ( u  =  ( d  i^i 
A )  ->  (
( ( cls `  K
) `  ( F " u ) )  C_  w 
<->  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )
7776biimpcd 232 . . . . . . . . . . . 12  |-  ( ( ( cls `  K
) `  ( F " u ) )  C_  w  ->  ( u  =  ( d  i^i  A
)  ->  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )
)
7877reximdv 2857 . . . . . . . . . . 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 436 . . . . . . . . 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 1290 . . . . . . . 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 776 . . . . . . . . . . 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 770 . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
x  e.  C  <->  y  e.  C ) )
8685anbi2d 718 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  y  e.  C ) ) )
87 sneq 3969 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  { x }  =  { y } )
8887fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { y } ) )
8988oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { y } )t  A ) )
9089oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) )
9190fveq1d 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F ) )
9291neeq1d 2702 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { y } )t  A ) ) `  F )  =/=  (/) ) )
9386, 92imbi12d 327 . . . . . . . . . . . . . . . . 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 2120 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F )  =/=  (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 21158 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
97 fvex 5889 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9897uniex 6606 . . . . . . . . . . . . . . . . 17  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9998snid 3988 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) }
10032adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  Haus )
10184eleq2d 2534 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( x  e.  ( ( cls `  J
) `  A )  <->  x  e.  C ) )
102101biimpar 493 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  ( ( cls `  J
) `  A )
)
10367adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  J  e.  (TopOn `  C )
)
10469adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  A  C_  C )
105 simpr 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  C )
106 trnei 20985 . . . . . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
x  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) ) )
108102, 107mpbid 215 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) )
10937adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  F : A --> B )
11046hausflf2 21091 . . . . . . . . . . . . . . . . . 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 1295 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  ~~  1o )
112 en1b 7655 . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) } )
11499, 113syl5eleqr 2556 . . . . . . . . . . . . . . 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 2549 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11646toptopon 20025 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  Top  <->  K  e.  (TopOn `  B ) )
11734, 116sylib 201 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  (TopOn `  B ) )
118117adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  (TopOn `  B )
)
119 flfnei 21084 . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . 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 470 . . . . . . . . . . . 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 2776 . . . . . . . . . . 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 673 . . . . . . . . . 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 744 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  K  e.  Top )
126 simplr 770 . . . . . . . . . . . . 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 20199 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  e.  ( ( nei `  K ) `  { ( ( ( JCnExt K ) `  F ) `  x
) } ) )  ->  b  C_  B
)
128125, 126, 127syl2anc 673 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  C_  B )
129 simpr 468 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
13046clsss 20146 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )
)
131 sstr 3426 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
132130, 131sylan 479 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u ) 
C_  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
1331323an1rs 1245 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( ( cls `  K
) `  b )  C_  w )  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
134133ex 441 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  C_  B  /\  (
( cls `  K
) `  b )  C_  w )  ->  (
( F " u
)  C_  b  ->  ( ( cls `  K
) `  ( F " u ) )  C_  w ) )
135134reximdv 2857 . . . . . . . . . . . 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 1292 . . . . . . . . . . 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 733 . . . . . . . . . 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 740 . . . . . . . . . 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 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  K  e.  Reg )
142141ad2antrr 740 . . . . . . . . . . . . 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 770 . . . . . . . . . . . . 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 772 . . . . . . . . . . . . 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 20427 . . . . . . . . . . . . 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 1292 . . . . . . . . . . . 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 3426 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  b )  C_  c  /\  c  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
148147expcom 442 . . . . . . . . . . . . . . 15  |-  ( c 
C_  w  ->  (
( ( cls `  K
) `  b )  C_  c  ->  ( ( cls `  K ) `  b )  C_  w
) )
149148anim2d 575 . . . . . . . . . . . . . 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 2857 . . . . . . . . . . . . 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 743 . . . . . . . . . . . 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 468 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
154 neii2 20201 . . . . . . . . . . . . 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 5889 . . . . . . . . . . . . . . . . 17  |-  ( ( ( JCnExt K ) `
 F ) `  x )  e.  _V
156155snss 4087 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( JCnExt K
) `  F ) `  x )  e.  c  <->  { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c
)
157156anbi1i 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w )  <->  ( {
( ( ( JCnExt
K ) `  F
) `  x ) }  C_  c  /\  c  C_  w ) )
158157biimpri 211 . . . . . . . . . . . . . 14  |-  ( ( { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c  /\  c  C_  w )  ->  ( ( ( ( JCnExt K ) `
 F ) `  x )  e.  c  /\  c  C_  w
) )
159158reximi 2852 . . . . . . . . . . . . 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 17 . . . . . . . . . . . 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 673 . . . . . . . . . . 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 2918 . . . . . . . . . 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 661 . . . . . . . . . . . 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 20212 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Top  /\  b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
1651643expib 1234 . . . . . . . . . . . . 13  |-  ( K  e.  Top  ->  (
( b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) ) )
166165anim1d 574 . . . . . . . . . . . 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 226 . . . . . . . . . . 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 2855 . . . . . . . . . 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 61 . . . . . . . . 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 2918 . . . . . . . 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 2918 . . . . . . 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 2918 . . . . . 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 770 . . . . . . . . . . 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 768 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  ph )
1754ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  J  e.  Top )
176 simplr 770 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  J )
17765eltopss 20014 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  Top  /\  v  e.  J )  ->  v  C_  C )
178175, 176, 177syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  C_  C )
179 simpr 468 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  v )
180178, 179sseldd 3419 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  C )
181 fvex 5889 . . . . . . . . . . . . . . 15  |-  ( ( nei `  J ) `
 { z } )  e.  _V
182181a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( nei `  J
) `  { z } )  e.  _V )
18370ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  A  e.  _V )
184 opnneip 20212 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { z } ) )
1854, 184syl3an1 1325 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
1861853expa 1231 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
187 elrestr 15405 . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . 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 21158 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  z )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
190189adantr 472 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  Haus )
19284eleq2d 2534 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( z  e.  ( ( cls `  J
) `  A )  <->  z  e.  C ) )
193192biimpar 493 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  ( ( cls `  J
) `  A )
)
19467adantr 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  J  e.  (TopOn `  C )
)
19569adantr 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  A  C_  C )
196 simpr 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  C )
197 trnei 20985 . . . . . . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  (
z  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) ) )
199193, 198mpbid 215 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) )
20037adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  F : A --> B )
201 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  e.  C  <->  z  e.  C ) )
202201anbi2d 718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  z  e.  C ) ) )
203 sneq 3969 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  { x }  =  { z } )
204203fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { z } ) )
205204oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
206205oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) )
207206fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
208207neeq1d 2702 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =/=  (/) ) )
209202, 208imbi12d 327 . . . . . . . . . . . . . . . . . . . 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 2120 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =/=  (/) )
21146hausflf2 21091 . . . . . . . . . . . . . . . . . . 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 1295 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o )
213 en1b 7655 . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) } )
215214adantr 472 . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  (TopOn `  B )
)
217 flfval 21083 . . . . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J ) `  {
z } )t  A ) ) ) )
219218adantr 472 . . . . . . . . . . . . . . . . 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 6607 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( K  e.  Haus  ->  U. K  e.  _V )
22132, 220syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U. K  e.  _V )
222221ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  U. K  e. 
_V )
22346, 222syl5eqel 2553 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  B  e.  _V )
224199adantr 472 . . . . . . . . . . . . . . . . . . . 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 20941 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A )  ->  ( ( ( nei `  J ) `
 { z } )t  A )  e.  (
fBas `  A )
)
226224, 225syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( (
( nei `  J
) `  { z } )t  A )  e.  (
fBas `  A )
)
22737ad2antrr 740 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  F : A
--> B )
228 simpr 468 . . . . . . . . . . . . . . . . . . . 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 20968 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A )  ->  ( A filGen ( ( ( nei `  J
) `  { z } )t  A ) )  =  ( ( ( nei `  J ) `  {
z } )t  A ) )
230199, 229syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  ( A filGen ( ( ( nei `  J ) `
 { z } )t  A ) )  =  ( ( ( nei `  J ) `  {
z } )t  A ) )
231230adantr 472 . . . . . . . . . . . . . . . . . . . 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 2552 . . . . . . . . . . . . . . . . . . 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 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )  =  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )
234233imaelfm 21044 . . . . . . . . . . . . . . . . . . 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 1295 . . . . . . . . . . . . . . . . . 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 21071 . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . 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 3452 . . . . . . . . . . . . . . . 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 3453 . . . . . . . . . . . . . . 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 5889 . . . . . . . . . . . . . . . . 17  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
241240uniex 6606 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
242241snss 4087 . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . 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 2549 . . . . . . . . . . . . 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 1291 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
246245adantlr 729 . . . . . . . . . . 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 3419 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  w
)
248247ralrimiva 2809 . . . . . . . . 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 630 . . . . . . . 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 2857 . . . . . . 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 740 . . . . . 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 21159 . . . . . . . . . 10  |-  ( ph  ->  ( ( JCnExt K
) `  F ) : C --> B )
254 ffun 5742 . . . . . . . . . 10  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  Fun  ( ( JCnExt K
) `  F )
)
255253, 254syl 17 . . . . . . . . 9  |-  ( ph  ->  Fun  ( ( JCnExt
K ) `  F
) )
256255adantr 472 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  Fun  ( ( JCnExt K
) `  F )
)
25765neii1 20199 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  v  e.  ( ( nei `  J ) `  { x } ) )  ->  v  C_  C )
2584, 257sylan 479 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  C )
259 fdm 5745 . . . . . . . . . . 11  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  dom  ( ( JCnExt K
) `  F )  =  C )
260253, 259syl 17 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( JCnExt
K ) `  F
)  =  C )
261260adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  dom  ( ( JCnExt K
) `  F )  =  C )
262258, 261sseqtr4d 3455 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  dom  ( ( JCnExt K ) `  F ) )
263 funimass4 5930 . . . . . . . 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 673 . . . . . . 7  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( ( ( JCnExt K ) `  F ) " v
)  C_  w  <->  A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
265264biimprd 231 . . . . . 6  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( A. z  e.  v  ( ( ( JCnExt K ) `  F ) `  z
)  e.  w  -> 
( ( ( JCnExt
K ) `  F
) " v ) 
C_  w ) )
266265reximdva 2858 . . . . 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 61 . . . 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 2809 . . 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 2809 . 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 20375 . . 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 1292 . 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 240 1  |-  ( ph  ->  ( ( JCnExt K
) `  F )  e.  ( J  Cn  K
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031    i^i cin 3389    C_ wss 3390   (/)c0 3722   {csn 3959   U.cuni 4190   class class class wbr 4395   dom cdm 4839   ran crn 4840   "cima 4842   Fun wfun 5583   -->wf 5585   ` cfv 5589  (class class class)co 6308   1oc1o 7193    ~~ cen 7584   ↾t crest 15397   fBascfbas 19035   filGencfg 19036   Topctop 19994  TopOnctopon 19995   clsccl 20110   neicnei 20190    Cn ccn 20317   Hauscha 20401   Regcreg 20402   Filcfil 20938    FilMap cfm 21026    fLim cflim 21027    fLimf cflf 21028  CnExtccnext 21152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-1o 7200  df-map 7492  df-pm 7493  df-en 7588  df-rest 15399  df-topgen 15420  df-fbas 19044  df-fg 19045  df-top 19998  df-topon 20000  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-cn 20320  df-cnp 20321  df-haus 20408  df-reg 20409  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-cnext 21153
This theorem is referenced by:  cnextucn  21396
  Copyright terms: Public domain W3C validator