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

Theorem cnextcn 20545
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 1005 . . . . . . . . 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 1004 . . . . . . . . . 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 19587 . . . . . . . . . 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 3098 . . . . . . . . . . . . . . . . . . . 20  |-  x  e. 
_V
109snss 4139 . . . . . . . . . . . . . . . . . . 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 978 . . . . . . . . . . . . . . . . 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 19598 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  Top  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { x }
) )
234, 22syl3an1 1262 . . . . . . . . . . . . . . . . 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 1004 . . . . . . . . . . . . . . . . . 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 19810 . . . . . . . . . . . . . . . . . . . 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 5338 . . . . . . . . . . . . . . . . . . . 20  |-  ( F
" ( d  i^i 
A ) )  C_  ran  F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : A --> B )
38 frn 5727 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : A --> B  ->  ran  F  C_  B )
3937, 38syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  F  C_  B
)
4036, 39syl5ss 3500 . . . . . . . . . . . . . . . . . . 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 3708 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  d  ->  (
v  i^i  A )  C_  ( d  i^i  A
) )
43 imass2 5362 . . . . . . . . . . . . . . . . . . . 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 19533 . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
49 sstr 3497 . . . . . . . . . . . . . . . . 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 804 . . . . . . . . . . . . . . 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 2914 . . . . . . . . . 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 1228 . . . . . . . 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 1219 . . . . . . 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 767 . . . . . . . . 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 755 . . . . . . . . 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 5866 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { x }
)  e.  _V
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( nei `  J
) `  { x } )  e.  _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17  |-  C  = 
U. J
6665toptopon 19412 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  <->  J  e.  (TopOn `  C ) )
674, 66sylib 196 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  (TopOn `  C ) )
6867elfvexd 5884 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  _V )
69 cnextf.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  C )
7068, 69ssexd 4584 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  _V )
71 elrest 14807 . . . . . . . . . . . . 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 5323 . . . . . . . . . . . . . . 15  |-  ( u  =  ( d  i^i 
A )  ->  ( F " u )  =  ( F " (
d  i^i  A )
) )
7574fveq2d 5860 . . . . . . . . . . . . . 14  |-  ( u  =  ( d  i^i 
A )  ->  (
( cls `  K
) `  ( F " u ) )  =  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
7675sseq1d 3516 . . . . . . . . . . . . 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 2917 . . . . . . . . . . 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 1227 . . . . . . . 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 759 . . . . . . . . . . 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 755 . . . . . . . . . . 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 2515 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
x  e.  C  <->  y  e.  C ) )
8685anbi2d 703 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  y  e.  C ) ) )
87 sneq 4024 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  { x }  =  { y } )
8887fveq2d 5860 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { y } ) )
8988oveq1d 6296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { y } )t  A ) )
9089oveq2d 6297 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) )
9190fveq1d 5858 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F ) )
9291neeq1d 2720 . . . . . . . . . . . . . . . . . 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 2000 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F )  =/=  (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 20543 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
97 fvex 5866 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9897uniex 6581 . . . . . . . . . . . . . . . . 17  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9998snid 4042 . . . . . . . . . . . . . . . 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 2513 . . . . . . . . . . . . . . . . . . . 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 20371 . . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . . 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 20477 . . . . . . . . . . . . . . . . . 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 1232 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  ~~  1o )
112 en1b 7585 . . . . . . . . . . . . . . . . 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 2538 . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11646toptopon 19412 . . . . . . . . . . . . . . . . 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 20470 . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . 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 2812 . . . . . . . . . . 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 755 . . . . . . . . . . . . 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 19585 . . . . . . . . . . . . 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 19533 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )
)
131 sstr 3497 . . . . . . . . . . . . . . . 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 1209 . . . . . . . . . . . . . 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 2917 . . . . . . . . . . . 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 1229 . . . . . . . . . . 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 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 ) )  -> 
c  e.  K )
144 simprl 756 . . . . . . . . . . . . 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 19813 . . . . . . . . . . . . 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 1229 . . . . . . . . . . . 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 3497 . . . . . . . . . . . . . . . 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 2917 . . . . . . . . . . . . 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 19587 . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . 17  |-  ( ( ( JCnExt K ) `
 F ) `  x )  e.  _V
156155snss 4139 . . . . . . . . . . . . . . . 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 2911 . . . . . . . . . . . . 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 2985 . . . . . . . . . 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 19598 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Top  /\  b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
1651643expib 1200 . . . . . . . . . . . . 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 2914 . . . . . . . . . 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 2985 . . . . . . . 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 2985 . . . . . . 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 2985 . . . . . 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 755 . . . . . . . . . . 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 755 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  J )
17765eltopss 19394 . . . . . . . . . . . . . . 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 3490 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  C )
181 fvex 5866 . . . . . . . . . . . . . . 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 19598 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { z } ) )
1854, 184syl3an1 1262 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
1861853expa 1197 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
187 elrestr 14808 . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . 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 20543 . . . . . . . . . . . . . . 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 2513 . . . . . . . . . . . . . . . . . . . . 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 20371 . . . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . . . 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 2515 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  e.  C  <->  z  e.  C ) )
202201anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  z  e.  C ) ) )
203 sneq 4024 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  { x }  =  { z } )
204203fveq2d 5860 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { z } ) )
205204oveq1d 6296 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
206205oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) )
207206fveq1d 5858 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
208207neeq1d 2720 . . . . . . . . . . . . . . . . . . . . 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 2000 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =/=  (/) )
21146hausflf2 20477 . . . . . . . . . . . . . . . . . . 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 1232 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o )
213 en1b 7585 . . . . . . . . . . . . . . . . . 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 20469 . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . 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 6582 . . . . . . . . . . . . . . . . . . . . . 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 2535 . . . . . . . . . . . . . . . . . . 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 20327 . . . . . . . . . . . . . . . . . . . 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 20354 . . . . . . . . . . . . . . . . . . . . . 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 2534 . . . . . . . . . . . . . . . . . . 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 20430 . . . . . . . . . . . . . . . . . . 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 1232 . . . . . . . . . . . . . . . . . 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 20457 . . . . . . . . . . . . . . . . . 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 3523 . . . . . . . . . . . . . . . 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 3524 . . . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . 17  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
241240uniex 6581 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
242241snss 4139 . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . 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 1228 . . . . . . . . . . . 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 3490 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  w
)
248247ralrimiva 2857 . . . . . . . . 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 2917 . . . . . . 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 20544 . . . . . . . . . 10  |-  ( ph  ->  ( ( JCnExt K
) `  F ) : C --> B )
254 ffun 5723 . . . . . . . . . 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 19585 . . . . . . . . . 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 5725 . . . . . . . . . . 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 3526 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  dom  ( ( JCnExt K ) `  F ) )
263 funimass4 5909 . . . . . . . 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 2918 . . . . 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 2857 . . 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 2857 . 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 19761 . . 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 1229 . 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 974    = wceq 1383    e. wcel 1804    =/= wne 2638   A.wral 2793   E.wrex 2794   _Vcvv 3095    i^i cin 3460    C_ wss 3461   (/)c0 3770   {csn 4014   U.cuni 4234   class class class wbr 4437   dom cdm 4989   ran crn 4990   "cima 4992   Fun wfun 5572   -->wf 5574   ` cfv 5578  (class class class)co 6281   1oc1o 7125    ~~ cen 7515   ↾t crest 14800   fBascfbas 18385   filGencfg 18386   Topctop 19372  TopOnctopon 19373   clsccl 19497   neicnei 19576    Cn ccn 19703   Hauscha 19787   Regcreg 19788   Filcfil 20324    FilMap cfm 20412    fLim cflim 20413    fLimf cflf 20414  CnExtccnext 20537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-1st 6785  df-2nd 6786  df-1o 7132  df-map 7424  df-pm 7425  df-en 7519  df-rest 14802  df-topgen 14823  df-fbas 18395  df-fg 18396  df-top 19377  df-topon 19380  df-cld 19498  df-ntr 19499  df-cls 19500  df-nei 19577  df-cn 19706  df-cnp 19707  df-haus 19794  df-reg 19795  df-fil 20325  df-fm 20417  df-flim 20418  df-flf 20419  df-cnext 20538
This theorem is referenced by:  cnextucn  20784
  Copyright terms: Public domain W3C validator