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

Theorem cnextcn 18136
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 732 . . . . 5  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  ph )
2 simpll 732 . . . . . . . . 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 966 . . . . . . . . 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 708 . . . . . . . . . 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 965 . . . . . . . . . 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 17210 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  d  e.  ( ( nei `  J ) `  { x } ) )  ->  E. v  e.  J  ( {
x }  C_  v  /\  v  C_  d ) )
85, 6, 7syl2anc 644 . . . . . . . . 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 2968 . . . . . . . . . . . . . . . . . . . 20  |-  x  e. 
_V
109snss 3955 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  v  <->  { x }  C_  v )
1110biimpri 199 . . . . . . . . . . . . . . . . . 18  |-  ( { x }  C_  v  ->  x  e.  v )
1211anim1i 553 . . . . . . . . . . . . . . . . 17  |-  ( ( { x }  C_  v  /\  v  C_  d
)  ->  ( x  e.  v  /\  v  C_  d ) )
1312anim2i 554 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) )  ->  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) )
1413anim2i 554 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d
) ) )  -> 
( ph  /\  (
v  e.  J  /\  ( x  e.  v  /\  v  C_  d ) ) ) )
1514ex 425 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) ) )
16 3anass 941 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  <->  ( ph  /\  ( v  e.  J  /\  x  e.  v
) ) )
1716anbi1i 678 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ( ph  /\  ( v  e.  J  /\  x  e.  v ) )  /\  v  C_  d ) )
18 anass 632 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
v  e.  J  /\  x  e.  v )
)  /\  v  C_  d )  <->  ( ph  /\  ( ( v  e.  J  /\  x  e.  v )  /\  v  C_  d ) ) )
19 anass 632 . . . . . . . . . . . . . . . . 17  |-  ( ( ( v  e.  J  /\  x  e.  v
)  /\  v  C_  d )  <->  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )
2019anbi2i 677 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
v  e.  J  /\  x  e.  v )  /\  v  C_  d ) )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
2117, 18, 203bitri 264 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  <->  ( ph  /\  ( v  e.  J  /\  ( x  e.  v  /\  v  C_  d
) ) ) )
22 opnneip 17221 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  Top  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { x }
) )
234, 22syl3an1 1218 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
2423adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  v  e.  ( ( nei `  J
) `  { x } ) )
25 simpr2 965 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  d  /\  ( ph  /\  v  e.  J  /\  x  e.  v ) )  -> 
v  e.  J )
2625ex 425 . . . . . . . . . . . . . . . . 17  |-  ( v 
C_  d  ->  (
( ph  /\  v  e.  J  /\  x  e.  v )  ->  v  e.  J ) )
2726imdistanri 674 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  J  /\  v  C_  d ) )
2824, 27jca 520 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J  /\  x  e.  v )  /\  v  C_  d )  ->  (
v  e.  ( ( nei `  J ) `
 { x }
)  /\  ( v  e.  J  /\  v  C_  d ) ) )
2921, 28sylbir 206 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( v  e.  J  /\  (
x  e.  v  /\  v  C_  d ) ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) )
3015, 29syl6 32 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( v  e.  J  /\  ( { x }  C_  v  /\  v  C_  d ) )  ->  ( v  e.  ( ( nei `  J
) `  { x } )  /\  (
v  e.  J  /\  v  C_  d ) ) ) )
3130adantr 453 . . . . . . . . . . . 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 17433 . . . . . . . . . . . . . . . . . . . 20  |-  ( K  e.  Haus  ->  K  e. 
Top )
3432, 33syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K  e.  Top )
3534adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  K  e.  Top )
36 imassrn 5249 . . . . . . . . . . . . . . . . . . . 20  |-  ( F
" ( d  i^i 
A ) )  C_  ran  F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : A --> B )
38 frn 5632 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F : A --> B  ->  ran  F  C_  B )
3937, 38syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  F  C_  B
)
4036, 39syl5ss 3348 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F " (
d  i^i  A )
)  C_  B )
4140adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( d  i^i 
A ) )  C_  B )
42 ssrin 3554 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  d  ->  (
v  i^i  A )  C_  ( d  i^i  A
) )
43 imass2 5275 . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  C_  d )  ->  ( F " ( v  i^i 
A ) )  C_  ( F " ( d  i^i  A ) ) )
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19  |-  B  = 
U. K
4746clsss 17156 . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
49 sstr 3345 . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  v  C_  d )  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5150an32s 781 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w )  /\  v  C_  d )  ->  (
( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )
5251ex 425 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )  ->  ( v  C_  d  ->  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w ) )
5352anim2d 550 . . . . . . . . . . . . 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 550 . . . . . . . . . . . 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 43 . . . . . . . . . . 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 2822 . . . . . . . . . 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 420 . . . . . . . . 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 1184 . . . . . . . 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 1176 . . . . . . 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 449 . . . . . . . . 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 744 . . . . . . . . 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 733 . . . . . . . . 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 5773 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { x }
)  e.  _V
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( nei `  J
) `  { x } )  e.  _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17  |-  C  = 
U. J
6665toptopon 17036 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  <->  J  e.  (TopOn `  C ) )
674, 66sylib 190 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  (TopOn `  C ) )
6867elfvexd 5790 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  _V )
69 cnextf.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  C )
7068, 69ssexd 4385 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  _V )
71 elrest 13693 . . . . . . . . . . . . 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 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  ( ( ( nei `  J
) `  { x } )t  A )  <->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) ) )
7372biimpa 472 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ( nei `  J ) `  {
x } )t  A ) )  ->  E. d  e.  ( ( nei `  J
) `  { x } ) u  =  ( d  i^i  A
) )
74 imaeq2 5234 . . . . . . . . . . . . . . 15  |-  ( u  =  ( d  i^i 
A )  ->  ( F " u )  =  ( F " (
d  i^i  A )
) )
7574fveq2d 5767 . . . . . . . . . . . . . 14  |-  ( u  =  ( d  i^i 
A )  ->  (
( cls `  K
) `  ( F " u ) )  =  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) ) )
7675sseq1d 3364 . . . . . . . . . . . . 13  |-  ( u  =  ( d  i^i 
A )  ->  (
( ( cls `  K
) `  ( F " u ) )  C_  w 
<->  ( ( cls `  K
) `  ( F " ( d  i^i  A
) ) )  C_  w ) )
7776biimpcd 217 . . . . . . . . . . . 12  |-  ( ( ( cls `  K
) `  ( F " u ) )  C_  w  ->  ( u  =  ( d  i^i  A
)  ->  ( ( cls `  K ) `  ( F " ( d  i^i  A ) ) )  C_  w )
)
7877reximdv 2824 . . . . . . . . . . 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 31 . . . . . . . . . 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 420 . . . . . . . . 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 1183 . . . . . . . 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 736 . . . . . . . . . . 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 733 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
84 cnextf.6 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( cls `  J
) `  A )  =  C )
85 eleq1 2503 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
x  e.  C  <->  y  e.  C ) )
8685anbi2d 686 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  y  e.  C ) ) )
87 sneq 3854 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  { x }  =  { y } )
8887fveq2d 5767 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { y } ) )
8988oveq1d 6132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { y } )t  A ) )
9089oveq2d 6133 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) )
9190fveq1d 5765 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F ) )
9291neeq1d 2621 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { y } )t  A ) ) `  F )  =/=  (/) ) )
9386, 92imbi12d 313 . . . . . . . . . . . . . . . . 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 1973 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { y } )t  A ) ) `  F )  =/=  (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 18134 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
97 fvex 5773 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9897uniex 4740 . . . . . . . . . . . . . . . . 17  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  _V
9998snid 3870 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) }
10032adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  Haus )
10184eleq2d 2510 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( x  e.  ( ( cls `  J
) `  A )  <->  x  e.  C ) )
102101biimpar 473 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  ( ( cls `  J
) `  A )
)
10367adantr 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  J  e.  (TopOn `  C )
)
10469adantr 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  A  C_  C )
105 simpr 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  C )
106 trnei 17962 . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  C )  ->  (
x  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) ) )
108102, 107mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( nei `  J
) `  { x } )t  A )  e.  ( Fil `  A ) )
10937adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  C )  ->  F : A --> B )
11046hausflf2 18068 . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  ~~  1o )
112 en1b 7211 . . . . . . . . . . . . . . . . 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 190 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) } )
11499, 113syl5eleqr 2530 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  U. (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11596, 114eqeltrd 2517 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  x )  e.  ( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F ) )
11646toptopon 17036 . . . . . . . . . . . . . . . . 17  |-  ( K  e.  Top  <->  K  e.  (TopOn `  B ) )
11734, 116sylib 190 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  (TopOn `  B ) )
118117adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  C )  ->  K  e.  (TopOn `  B )
)
119 flfnei 18061 . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 2811 . . . . . . . . . . 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 644 . . . . . . . . . 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 712 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  K  e.  Top )
126 simplr 733 . . . . . . . . . . . . 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 17208 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  e.  ( ( nei `  K ) `  { ( ( ( JCnExt K ) `  F ) `  x
) } ) )  ->  b  C_  B
)
128125, 126, 127syl2anc 644 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  b  C_  B )
129 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  C )  /\  b  e.  (
( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  ( ( cls `  K ) `
 b )  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
13046clsss 17156 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )
)
131 sstr 3345 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  ( F " u ) )  C_  ( ( cls `  K
) `  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
132130, 131sylan 459 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( F " u ) 
C_  b )  /\  ( ( cls `  K
) `  b )  C_  w )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
1331323an1rs 1166 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  Top  /\  b  C_  B  /\  ( ( cls `  K
) `  b )  C_  w )  /\  ( F " u )  C_  b )  ->  (
( cls `  K
) `  ( F " u ) )  C_  w )
134133ex 425 . . . . . . . . . . . . 13  |-  ( ( K  e.  Top  /\  b  C_  B  /\  (
( cls `  K
) `  b )  C_  w )  ->  (
( F " u
)  C_  b  ->  ( ( cls `  K
) `  ( F " u ) )  C_  w ) )
135134reximdv 2824 . . . . . . . . . . . 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 1185 . . . . . . . . . . 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 701 . . . . . . . . . 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 708 . . . . . . . . . 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 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  K  e.  Reg )
142141ad2antrr 708 . . . . . . . . . . . . 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 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  /\  c  e.  K )  /\  (
( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w ) )  -> 
c  e.  K )
144 simprl 734 . . . . . . . . . . . . 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 17436 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 3345 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( cls `  K
) `  b )  C_  c  /\  c  C_  w )  ->  (
( cls `  K
) `  b )  C_  w )
148147expcom 426 . . . . . . . . . . . . . . 15  |-  ( c 
C_  w  ->  (
( ( cls `  K
) `  b )  C_  c  ->  ( ( cls `  K ) `  b )  C_  w
) )
149148anim2d 550 . . . . . . . . . . . . . 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 2824 . . . . . . . . . . . . 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 711 . . . . . . . . . . . 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 449 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  C )  /\  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )  ->  w  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
154 neii2 17210 . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . . . . 17  |-  ( ( ( JCnExt K ) `
 F ) `  x )  e.  _V
156155snss 3955 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( JCnExt K
) `  F ) `  x )  e.  c  <->  { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c
)
157156anbi1i 678 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( JCnExt
K ) `  F
) `  x )  e.  c  /\  c  C_  w )  <->  ( {
( ( ( JCnExt
K ) `  F
) `  x ) }  C_  c  /\  c  C_  w ) )
158157biimpri 199 . . . . . . . . . . . . . 14  |-  ( ( { ( ( ( JCnExt K ) `  F ) `  x
) }  C_  c  /\  c  C_  w )  ->  ( ( ( ( JCnExt K ) `
 F ) `  x )  e.  c  /\  c  C_  w
) )
159158reximi 2820 . . . . . . . . . . . . 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 644 . . . . . . . . . . 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 2857 . . . . . . . . . 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 632 . . . . . . . . . . . 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 17221 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Top  /\  b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) )
1651643expib 1157 . . . . . . . . . . . . 13  |-  ( K  e.  Top  ->  (
( b  e.  K  /\  ( ( ( JCnExt
K ) `  F
) `  x )  e.  b )  ->  b  e.  ( ( nei `  K
) `  { (
( ( JCnExt K
) `  F ) `  x ) } ) ) )
166165anim1d 549 . . . . . . . . . . . 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 211 . . . . . . . . . . 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 2822 . . . . . . . . . 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 59 . . . . . . . . 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 2857 . . . . . . . 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 2857 . . . . . . 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 2857 . . . . . 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 733 . . . . . . . . . . 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 732 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  ph )
1754ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  J  e.  Top )
176 simplr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  J )
17765eltopss 17018 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  Top  /\  v  e.  J )  ->  v  C_  C )
178175, 176, 177syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  C_  C )
179 simpr 449 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  v )
180178, 179sseldd 3338 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  z  e.  C )
181 fvex 5773 . . . . . . . . . . . . . . 15  |-  ( ( nei `  J ) `
 { z } )  e.  _V
182181a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( nei `  J
) `  { z } )  e.  _V )
18370ad2antrr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  A  e.  _V )
184 opnneip 17221 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J ) `
 { z } ) )
1854, 184syl3an1 1218 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  J  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
1861853expa 1154 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  v  e.  ( ( nei `  J
) `  { z } ) )
187 elrestr 13694 . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . 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 18134 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( JCnExt K
) `  F ) `  z )  =  U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
190189adantr 453 . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  Haus )
19284eleq2d 2510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( z  e.  ( ( cls `  J
) `  A )  <->  z  e.  C ) )
193192biimpar 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  ( ( cls `  J
) `  A )
)
19467adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  J  e.  (TopOn `  C )
)
19569adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  A  C_  C )
196 simpr 449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  C )  ->  z  e.  C )
197 trnei 17962 . . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  C )  ->  (
z  e.  ( ( cls `  J ) `
 A )  <->  ( (
( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) ) )
199193, 198mpbid 203 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( ( nei `  J
) `  { z } )t  A )  e.  ( Fil `  A ) )
20037adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  F : A --> B )
201 eleq1 2503 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
x  e.  C  <->  z  e.  C ) )
202201anbi2d 686 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ph  /\  x  e.  C )  <->  ( ph  /\  z  e.  C ) ) )
203 sneq 3854 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  z  ->  { x }  =  { z } )
204203fveq2d 5767 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  z  ->  (
( nei `  J
) `  { x } )  =  ( ( nei `  J
) `  { z } ) )
205204oveq1d 6132 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  z  ->  (
( ( nei `  J
) `  { x } )t  A )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
206205oveq2d 6133 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  z  ->  ( K  fLimf  ( ( ( nei `  J ) `
 { x }
)t 
A ) )  =  ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) )
207206fveq1d 5765 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  z  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =  ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) )
208207neeq1d 2621 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
( ( K  fLimf  ( ( ( nei `  J
) `  { x } )t  A ) ) `  F )  =/=  (/)  <->  ( ( K  fLimf  ( ( ( nei `  J ) `
 { z } )t  A ) ) `  F )  =/=  (/) ) )
209202, 208imbi12d 313 . . . . . . . . . . . . . . . . . . . 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 1973 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =/=  (/) )
21146hausflf2 18068 . . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  ~~  1o )
213 en1b 7211 . . . . . . . . . . . . . . . . . 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 190 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  { U. ( ( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F ) } )
215214adantr 453 . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  C )  ->  K  e.  (TopOn `  B )
)
217 flfval 18060 . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  C )  ->  (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  =  ( K  fLim  ( ( B  FilMap  F ) `  ( ( ( nei `  J ) `  {
z } )t  A ) ) ) )
219218adantr 453 . . . . . . . . . . . . . . . . 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 4741 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( K  e.  Haus  ->  U. K  e.  _V )
22132, 220syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U. K  e.  _V )
222221ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  U. K  e. 
_V )
22346, 222syl5eqel 2527 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  B  e.  _V )
224199adantr 453 . . . . . . . . . . . . . . . . . . . 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 17918 . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  F : A
--> B )
228 simpr 449 . . . . . . . . . . . . . . . . . . . 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 17945 . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( A filGen ( ( ( nei `  J ) `  {
z } )t  A ) )  =  ( ( ( nei `  J
) `  { z } )t  A ) )
232228, 231eleqtrrd 2520 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( v  i^i  A )  e.  ( A filGen ( ( ( nei `  J ) `
 { z } )t  A ) ) )
233 eqid 2443 . . . . . . . . . . . . . . . . . . . 20  |-  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )  =  ( A
filGen ( ( ( nei `  J ) `  {
z } )t  A ) )
234233imaelfm 18021 . . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . . 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 18048 . . . . . . . . . . . . . . . . . 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 3371 . . . . . . . . . . . . . . . 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 3372 . . . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . . . . 17  |-  ( ( K  fLimf  ( (
( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
241240uniex 4740 . . . . . . . . . . . . . . . 16  |-  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  _V
242241snss 3955 . . . . . . . . . . . . . . 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 205 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  U. (
( K  fLimf  ( ( ( nei `  J
) `  { z } )t  A ) ) `  F )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
244190, 243eqeltrd 2517 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  C )  /\  (
v  i^i  A )  e.  ( ( ( nei `  J ) `  {
z } )t  A ) )  ->  ( (
( JCnExt K ) `
 F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
245174, 180, 188, 244syl21anc 1184 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  v  e.  J )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) ) )
246245adantlr 697 . . . . . . . . . . 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 3338 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  v  e.  J )  /\  ( ( cls `  K
) `  ( F " ( v  i^i  A
) ) )  C_  w )  /\  z  e.  v )  ->  (
( ( JCnExt K
) `  F ) `  z )  e.  w
)
248247ralrimiva 2796 . . . . . . . . 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 603 . . . . . . . 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 2824 . . . . . . 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 708 . . . . . 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 18135 . . . . . . . . . 10  |-  ( ph  ->  ( ( JCnExt K
) `  F ) : C --> B )
254 ffun 5628 . . . . . . . . . 10  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  Fun  ( ( JCnExt K
) `  F )
)
255253, 254syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  ( ( JCnExt
K ) `  F
) )
256255adantr 453 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  Fun  ( ( JCnExt K
) `  F )
)
25765neii1 17208 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  v  e.  ( ( nei `  J ) `  { x } ) )  ->  v  C_  C )
2584, 257sylan 459 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  C )
259 fdm 5630 . . . . . . . . . . 11  |-  ( ( ( JCnExt K ) `
 F ) : C --> B  ->  dom  ( ( JCnExt K
) `  F )  =  C )
260253, 259syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( JCnExt
K ) `  F
)  =  C )
261260adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  ->  dom  ( ( JCnExt K
) `  F )  =  C )
262258, 261sseqtr4d 3374 . . . . . . . 8  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
v  C_  dom  ( ( JCnExt K ) `  F ) )
263 funimass4 5813 . . . . . . . 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 644 . . . . . . 7  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( ( ( ( JCnExt K ) `  F ) " v
)  C_  w  <->  A. z  e.  v  ( (
( JCnExt K ) `
 F ) `  z )  e.  w
) )
265264biimprd 216 . . . . . 6  |-  ( (
ph  /\  v  e.  ( ( nei `  J
) `  { x } ) )  -> 
( A. z  e.  v  ( ( ( JCnExt K ) `  F ) `  z
)  e.  w  -> 
( ( ( JCnExt
K ) `  F
) " v ) 
C_  w ) )
266265reximdva 2825 . . . . 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 59 . . . 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 2796 . . 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 2796 . 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 17384 . . 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 1185 . 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 225 1  |-  ( ph  ->  ( ( JCnExt K
) `  F )  e.  ( J  Cn  K
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    = wceq 1654    e. wcel 1728    =/= wne 2606   A.wral 2712   E.wrex 2713   _Vcvv 2965    i^i cin 3308    C_ wss 3309   (/)c0 3616   {csn 3843   U.cuni 4044   class class class wbr 4243   dom cdm 4913   ran crn 4914   "cima 4916   Fun wfun 5483   -->wf 5485   ` cfv 5489  (class class class)co 6117   1oc1o 6753    ~~ cen 7142   ↾t crest 13686   fBascfbas 16727   filGencfg 16728   Topctop 16996  TopOnctopon 16997   clsccl 17120   neicnei 17199    Cn ccn 17326   Hauscha 17410   Regcreg 17411   Filcfil 17915    FilMap cfm 18003    fLim cflim 18004    fLimf cflf 18005  CnExtccnext 18128
This theorem is referenced by:  cnextucn  18371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-iin 4125  df-br 4244  df-opab 4298  df-mpt 4299  df-id 4533  df-suc 4622  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-1o 6760  df-map 7056  df-pm 7057  df-en 7146  df-rest 13688  df-topgen 13705  df-fbas 16737  df-fg 16738  df-top 17001  df-topon 17004  df-cld 17121  df-ntr 17122  df-cls 17123  df-nei 17200  df-cn 17329  df-cnp 17330  df-haus 17417  df-reg 17418  df-fil 17916  df-fm 18008  df-flim 18009  df-flf 18010  df-cnext 18129
  Copyright terms: Public domain W3C validator