MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnextcn Structured version   Unicode version
Theorem cnextcn 20299
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 1004 . . . . . . . . 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 1003 . . . . . . . . . 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 19372 . . . . . . . . . 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 3116 . . . . . . . . . . . . . . . . . . . 20 |- x e. _V
109snss 4151 . . . . . . . . . . . . . . . . . . 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 977 . . . . . . . . . . . . . . . . 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 19383 . . . . . . . . . . . . . . . . . 18 |- ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
234, 22syl3an1 1261 . . . . . . . . . . . . . . . . 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 1003 . . . . . . . . . . . . . . . . . 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 19595 . . . . . . . . . . . . . . . . . . . 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 5346 . . . . . . . . . . . . . . . . . . . 20 |- ( F " ( d i^i A ) ) C_ ran F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F : A --> B )
38 frn 5735 . . . . . . . . . . . . . . . . . . . . 21 |- ( F : A --> B -> ran F C_ B )
3937, 38syl 16 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran F C_ B )
4036, 39syl5ss 3515 . . . . . . . . . . . . . . . . . . 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 3723 . . . . . . . . . . . . . . . . . . . 20 |- ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) )
43 imass2 5370 . . . . . . . . . . . . . . . . . . . 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 19318 . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
49 sstr 3512 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
5048, 49sylan 471 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v C_ d ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
5150an32s 802 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
5251ex 434 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( v C_ d -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
5352anim2d 565 . . . . . . . . . . . . 13 |- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. J /\ v C_ d ) -> ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) )
5453anim2d 565 . . . . . . . . . . . 12 |- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) ) )
5531, 54syld 44 . . . . . . . . . . 11 |- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) ) ) )
5655reximdv2 2934 . . . . . . . . . 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 1227 . . . . . . . 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 1218 . . . . . . 7 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ d e. ( ( nei ` J ) ` { x } ) ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
60 simpr 461 . . . . . . . . 9 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
61 simp-4l 765 . . . . . . . . 9 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> ph )
62 simplr 754 . . . . . . . . 9 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) )
63 fvex 5874 . . . . . . . . . . . . . 14 |- ( ( nei ` J ) ` { x } ) e. _V
6463a1i 11 . . . . . . . . . . . . 13 |- ( ph -> ( ( nei ` J ) ` { x } ) e. _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17 |- C = U. J
6665toptopon 19198 . . . . . . . . . . . . . . . 16 |- ( J e. Top <-> J e. (TopOn ` C ) )
674, 66sylib 196 . . . . . . . . . . . . . . 15 |- ( ph -> J e. (TopOn ` C ) )
6867elfvexd 5892 . . . . . . . . . . . . . 14 |- ( ph -> C e. _V )
69 cnextf.a . . . . . . . . . . . . . 14 |- ( ph -> A C_ C )
7068, 69ssexd 4594 . . . . . . . . . . . . 13 |- ( ph -> A e. _V )
71 elrest 14676 . . . . . . . . . . . . 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 5331 . . . . . . . . . . . . . . 15 |- ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) )
7574fveq2d 5868 . . . . . . . . . . . . . 14 |- ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
7675sseq1d 3531 . . . . . . . . . . . . 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 2937 . . . . . . . . . . 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 1226 . . . . . . . 8 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> E. d e. ( ( nei ` J ) ` { x } ) ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w )
82 simplll 757 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ph /\ x e. C ) )
83 simplr 754 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
84 cnextf.6 . . . . . . . . . . . . . . . 16 |- ( ph -> ( ( cls ` J ) ` A ) = C )
85 eleq1 2539 . . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( x e. C <-> y e. C ) )
8685anbi2d 703 . . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
87 sneq 4037 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> { x } = { y } )
8887fveq2d 5868 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
8988oveq1d 6297 . . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { y } ) ↾t A ) )
9089oveq2d 6298 . . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) )
9190fveq1d 5866 . . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) )
9291neeq1d 2744 . . . . . . . . . . . . . . . . . 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 1983 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 20297 . . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
97 fvex 5874 . . . . . . . . . . . . . . . . . 18 |- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
9897uniex 6578 . . . . . . . . . . . . . . . . 17 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
9998snid 4055 . . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . . 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 20125 . . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . 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 20231 . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ~~ 1o )
112 en1b 7580 . . . . . . . . . . . . . . . . 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 2562 . . . . . . . . . . . . . . 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 2555 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
11646toptopon 19198 . . . . . . . . . . . . . . . . 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 20224 . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . 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 2833 . . . . . . . . . . 11 |- ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( F " u ) C_ b )
12482, 83, 123syl2anc 661 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( F " u ) C_ b )
12534ad3antrrr 729 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> K e. Top )
126 simplr 754 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
12746neii1 19370 . . . . . . . . . . . . 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 19318 . . . . . . . . . . . . . . . 16 |- ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) )
131 sstr 3512 . . . . . . . . . . . . . . . 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 1208 . . . . . . . . . . . . . 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 2937 . . . . . . . . . . . 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 1228 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( F " u ) C_ b -> E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) )
137136adantllr 718 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( F " u ) C_ b -> E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w ) )
138124, 137mpd 15 . . . . . . . . 9 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w )
13934ad2antrr 725 . . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Top )
140 cnextcn.8 . . . . . . . . . . . . . . 15 |- ( ph -> K e. Reg )
141140ad2antrr 725 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Reg )
142141ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> K e. Reg )
143 simplr 754 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> c e. K )
144 simprl 755 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. c )
145 regsep 19598 . . . . . . . . . . . . 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 1228 . . . . . . . . . . . 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 3512 . . . . . . . . . . . . . . . 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 2937 . . . . . . . . . . . . 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 19372 . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . . . . . 17 |- ( ( ( JCnExt K ) ` F ) ` x ) e. _V
156155snss 4151 . . . . . . . . . . . . . . . 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 2932 . . . . . . . . . . . . 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 3003 . . . . . . . . . 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 19383 . . . . . . . . . . . . . 14 |- ( ( K e. Top /\ b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
1651643expib 1199 . . . . . . . . . . . . 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 2934 . . . . . . . . . 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 3003 . . . . . . . 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 3003 . . . . . . 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 3003 . . . . . 6 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
173 simplr 754 . . . . . . . . . . 11 |- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
174 simpll 753 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph )
1754ad2antrr 725 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> J e. Top )
176 simplr 754 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. J )
17765eltopss 19180 . . . . . . . . . . . . . . 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 3505 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C )
181 fvex 5874 . . . . . . . . . . . . . . 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 19383 . . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
1854, 184syl3an1 1261 . . . . . . . . . . . . . . 15 |- ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
1861853expa 1196 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
187 elrestr 14677 . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . 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 20297 . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . . . 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 20125 . . . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . . 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 2539 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x e. C <-> z e. C ) )
202201anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) )
203 sneq 4037 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = z -> { x } = { z } )
204203fveq2d 5868 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
205204oveq1d 6297 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = z -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
206205oveq2d 6298 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) )
207206fveq1d 5866 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
208207neeq1d 2744 . . . . . . . . . . . . . . . . . . . . 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 1983 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) )
21146hausflf2 20231 . . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) ~~ 1o )
213 en1b 7580 . . . . . . . . . . . . . . . . . 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 20223 . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . 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 6579 . . . . . . . . . . . . . . . . . . . . . 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 2559 . . . . . . . . . . . . . . . . . . 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 20081 . . . . . . . . . . . . . . . . . . . 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 20108 . . . . . . . . . . . . . . . . . . . . . 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 2558 . . . . . . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . . . . . . . . 20 |- ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) )
234233imaelfm 20184 . . . . . . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . . . . . . 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 20211 . . . . . . . . . . . . . . . . . 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 3538 . . . . . . . . . . . . . . . 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 3539 . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . . . . . 17 |- ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
241240uniex 6578 . . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
242241snss 4151 . . . . . . . . . . . . . . 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 2555 . . . . . . . . . . . . 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 1227 . . . . . . . . . . . 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 3505 . . . . . . . . . 10 |- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. w )
248247ralrimiva 2878 . . . . . . . . 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 2937 . . . . . . 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 20298 . . . . . . . . . 10 |- ( ph -> ( ( JCnExt K ) ` F ) : C --> B )
254 ffun 5731 . . . . . . . . . 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 19370 . . . . . . . . . 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 5733 . . . . . . . . . . 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 3541 . . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( JCnExt K ) ` F ) )
263 funimass4 5916 . . . . . . . 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 2938 . . . . 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 2878 . . 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 2878 . 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 19546 . . 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 1228 . 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 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   i^i cin 3475   C_ wss 3476   (/)c0 3785   {csn 4027   U.cuni 4245   class class class wbr 4447   dom cdm 4999   ran crn 5000   "cima 5002   Fun wfun 5580   -->wf 5582   ` cfv 5586  (class class class)co 6282   1oc1o 7120   ~~ cen 7510   ↾t crest 14669   fBascfbas 18174   filGencfg 18175   Topctop 19158  TopOnctopon 19159   clsccl 19282   neicnei 19361   Cn ccn 19488   Hauscha 19572   Regcreg 19573   Filcfil 20078   FilMap cfm 20166   fLim cflim 20167   fLimf cflf 20168  CnExtccnext 20291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-1st 6781  df-2nd 6782  df-1o 7127  df-map 7419  df-pm 7420  df-en 7514  df-rest 14671  df-topgen 14692  df-fbas 18184  df-fg 18185  df-top 19163  df-topon 19166  df-cld 19283  df-ntr 19284  df-cls 19285  df-nei 19362  df-cn 19491  df-cnp 19492  df-haus 19579  df-reg 19580  df-fil 20079  df-fm 20171  df-flim 20172  df-flf 20173  df-cnext 20292
This theorem is referenced by:  cnextucn  20538
  Copyright terms: Public domain W3C validator