MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnextcn Structured version   Unicode version
Theorem cnextcn 20857
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 752 . . . . 5 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> ph )
2 simpll 752 . . . . . . . . 9 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ph )
3 simpr3 1005 . . . . . . . . 9 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w )
4 cnextf.3 . . . . . . . . . . 11 |- ( ph -> J e. Top )
54ad2antrr 724 . . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> J e. Top )
6 simpr2 1004 . . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> d e. ( ( nei ` J ) ` { x } ) )
7 neii2 19900 . . . . . . . . . 10 |- ( ( J e. Top /\ d e. ( ( nei ` J ) ` { x } ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) )
85, 6, 7syl2anc 659 . . . . . . . . 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 3061 . . . . . . . . . . . . . . . . . . . 20 |- x e. _V
109snss 4095 . . . . . . . . . . . . . . . . . . 19 |- ( x e. v <-> { x } C_ v )
1110biimpri 206 . . . . . . . . . . . . . . . . . 18 |- ( { x } C_ v -> x e. v )
1211anim1i 566 . . . . . . . . . . . . . . . . 17 |- ( ( { x } C_ v /\ v C_ d ) -> ( x e. v /\ v C_ d ) )
1312anim2i 567 . . . . . . . . . . . . . . . 16 |- ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
1413anim2i 567 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
1514ex 432 . . . . . . . . . . . . . 14 |- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) )
16 3anass 978 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) <-> ( ph /\ ( v e. J /\ x e. v ) ) )
1716anbi1i 693 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) )
18 anass 647 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) <-> ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) )
19 anass 647 . . . . . . . . . . . . . . . . 17 |- ( ( ( v e. J /\ x e. v ) /\ v C_ d ) <-> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
2019anbi2i 692 . . . . . . . . . . . . . . . 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 19911 . . . . . . . . . . . . . . . . . 18 |- ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
234, 22syl3an1 1263 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
2423adantr 463 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> v e. ( ( nei ` J ) ` { x } ) )
25 simpr2 1004 . . . . . . . . . . . . . . . . . 18 |- ( ( v C_ d /\ ( ph /\ v e. J /\ x e. v ) ) -> v e. J )
2625ex 432 . . . . . . . . . . . . . . . . 17 |- ( v C_ d -> ( ( ph /\ v e. J /\ x e. v ) -> v e. J ) )
2726imdistanri 689 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. J /\ v C_ d ) )
2824, 27jca 530 . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . 13 |- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) )
3130adantr 463 . . . . . . . . . . . 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 20123 . . . . . . . . . . . . . . . . . . . 20 |- ( K e. Haus -> K e. Top )
3432, 33syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. Top )
3534adantr 463 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> K e. Top )
36 imassrn 5167 . . . . . . . . . . . . . . . . . . . 20 |- ( F " ( d i^i A ) ) C_ ran F
37 cnextf.5 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F : A --> B )
38 frn 5719 . . . . . . . . . . . . . . . . . . . . 21 |- ( F : A --> B -> ran F C_ B )
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran F C_ B )
4036, 39syl5ss 3452 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( F " ( d i^i A ) ) C_ B )
4140adantr 463 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> ( F " ( d i^i A ) ) C_ B )
42 ssrin 3663 . . . . . . . . . . . . . . . . . . . 20 |- ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) )
43 imass2 5191 . . . . . . . . . . . . . . . . . . . 20 |- ( ( v i^i A ) C_ ( d i^i A ) -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( v C_ d -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
4544adantl 464 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
46 cnextf.2 . . . . . . . . . . . . . . . . . . 19 |- B = U. K
4746clsss 19845 . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
49 sstr 3449 . . . . . . . . . . . . . . . . 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 469 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v C_ d ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
5150an32s 805 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
5251ex 432 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( v C_ d -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
5352anim2d 563 . . . . . . . . . . . . 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 563 . . . . . . . . . . . 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 42 . . . . . . . . . . 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 2874 . . . . . . . . . 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 427 . . . . . . . . 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 1229 . . . . . . . 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 1220 . . . . . . 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 459 . . . . . . . . 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 768 . . . . . . . . 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 5858 . . . . . . . . . . . . . 14 |- ( ( nei ` J ) ` { x } ) e. _V
6463a1i 11 . . . . . . . . . . . . 13 |- ( ph -> ( ( nei ` J ) ` { x } ) e. _V )
65 cnextf.1 . . . . . . . . . . . . . . . . 17 |- C = U. J
6665toptopon 19724 . . . . . . . . . . . . . . . 16 |- ( J e. Top <-> J e. (TopOn ` C ) )
674, 66sylib 196 . . . . . . . . . . . . . . 15 |- ( ph -> J e. (TopOn ` C ) )
6867elfvexd 5876 . . . . . . . . . . . . . 14 |- ( ph -> C e. _V )
69 cnextf.a . . . . . . . . . . . . . 14 |- ( ph -> A C_ C )
7068, 69ssexd 4540 . . . . . . . . . . . . 13 |- ( ph -> A e. _V )
71 elrest 15040 . . . . . . . . . . . . 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 659 . . . . . . . . . . . 12 |- ( ph -> ( u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) )
7372biimpa 482 . . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) -> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) )
74 imaeq2 5152 . . . . . . . . . . . . . . 15 |- ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) )
7574fveq2d 5852 . . . . . . . . . . . . . 14 |- ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
7675sseq1d 3468 . . . . . . . . . . . . 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 2877 . . . . . . . . . . 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 30 . . . . . . . . . 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 427 . . . . . . . . 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 1228 . . . . . . . 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 760 . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( x e. C <-> y e. C ) )
8685anbi2d 702 . . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
87 sneq 3981 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> { x } = { y } )
8887fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
8988oveq1d 6292 . . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { y } ) ↾t A ) )
9089oveq2d 6293 . . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) )
9190fveq1d 5850 . . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) )
9291neeq1d 2680 . . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) ) )
9386, 92imbi12d 318 . . . . . . . . . . . . . . . . 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 2041 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) )
9665, 46, 4, 32, 37, 69, 84, 95cnextfvval 20855 . . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
97 fvex 5858 . . . . . . . . . . . . . . . . . 18 |- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
9897uniex 6577 . . . . . . . . . . . . . . . . 17 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
9998snid 3999 . . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) }
10032adantr 463 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> K e. Haus )
10184eleq2d 2472 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
102101biimpar 483 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
10367adantr 463 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> J e. (TopOn ` C ) )
10469adantr 463 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> A C_ C )
105 simpr 459 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> x e. C )
106 trnei 20683 . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> F : A --> B )
11046hausflf2 20789 . . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ~~ 1o )
112 en1b 7620 . . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . . 14 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
11646toptopon 19724 . . . . . . . . . . . . . . . . 17 |- ( K e. Top <-> K e. (TopOn ` B ) )
11734, 116sylib 196 . . . . . . . . . . . . . . . 16 |- ( ph -> K e. (TopOn ` B ) )
118117adantr 463 . . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> K e. (TopOn ` B ) )
119 flfnei 20782 . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . 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 461 . . . . . . . . . . . 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 2772 . . . . . . . . . . 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 659 . . . . . . . . . 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 728 . . . . . . . . . . . 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 19898 . . . . . . . . . . . . 13 |- ( ( K e. Top /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> b C_ B )
128125, 126, 127syl2anc 659 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b C_ B )
129 simpr 459 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
13046clsss 19845 . . . . . . . . . . . . . . . 16 |- ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) )
131 sstr 3449 . . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
132130, 131sylan 469 . . . . . . . . . . . . . . 15 |- ( ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
1331323an1rs 1209 . . . . . . . . . . . . . 14 |- ( ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
134133ex 432 . . . . . . . . . . . . 13 |- ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( F " u ) C_ b -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) )
135134reximdv 2877 . . . . . . . . . . . 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 1230 . . . . . . . . . . 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 717 . . . . . . . . . 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 724 . . . . . . . . . 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 724 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Reg )
142141ad2antrr 724 . . . . . . . . . . . . 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 756 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. c )
145 regsep 20126 . . . . . . . . . . . . 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 1230 . . . . . . . . . . . 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 3449 . . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` b ) C_ c /\ c C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
148147expcom 433 . . . . . . . . . . . . . . 15 |- ( c C_ w -> ( ( ( cls ` K ) ` b ) C_ c -> ( ( cls ` K ) ` b ) C_ w ) )
149148anim2d 563 . . . . . . . . . . . . . 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 2877 . . . . . . . . . . . . 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 727 . . . . . . . . . . . 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 459 . . . . . . . . . . . 12 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
154 neii2 19900 . . . . . . . . . . . . 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 5858 . . . . . . . . . . . . . . . . 17 |- ( ( ( JCnExt K ) ` F ) ` x ) e. _V
156155snss 4095 . . . . . . . . . . . . . . . 16 |- ( ( ( ( JCnExt K ) ` F ) ` x ) e. c <-> { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c )
157156anbi1i 693 . . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . . 13 |- ( E. c e. K ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> E. c e. K ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
160154, 159syl 17 . . . . . . . . . . . 12 |- ( ( K e. Top /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
161139, 153, 160syl2anc 659 . . . . . . . . . . 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 2948 . . . . . . . . . 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 647 . . . . . . . . . . . 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 19911 . . . . . . . . . . . . . 14 |- ( ( K e. Top /\ b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
1651643expib 1200 . . . . . . . . . . . . 13 |- ( K e. Top -> ( ( b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) )
166165anim1d 562 . . . . . . . . . . . 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 2874 . . . . . . . . . 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 2948 . . . . . . . 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 2948 . . . . . . 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 2948 . . . . . 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 752 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph )
1754ad2antrr 724 . . . . . . . . . . . . . . 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 19706 . . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ v e. J ) -> v C_ C )
178175, 176, 177syl2anc 659 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v C_ C )
179 simpr 459 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. v )
180178, 179sseldd 3442 . . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C )
181 fvex 5858 . . . . . . . . . . . . . . 15 |- ( ( nei ` J ) ` { z } ) e. _V
182181a1i 11 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( nei ` J ) ` { z } ) e. _V )
18370ad2antrr 724 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> A e. _V )
184 opnneip 19911 . . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
1854, 184syl3an1 1263 . . . . . . . . . . . . . . 15 |- ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
1861853expa 1197 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
187 elrestr 15041 . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . 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 20855 . . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. C ) -> ( ( ( JCnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
190189adantr 463 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. Haus )
19284eleq2d 2472 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( z e. ( ( cls ` J ) ` A ) <-> z e. C ) )
193192biimpar 483 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> z e. ( ( cls ` J ) ` A ) )
19467adantr 463 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> J e. (TopOn ` C ) )
19569adantr 463 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> A C_ C )
196 simpr 459 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> z e. C )
197 trnei 20683 . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> F : A --> B )
201 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x e. C <-> z e. C ) )
202201anbi2d 702 . . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) )
203 sneq 3981 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = z -> { x } = { z } )
204203fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
205204oveq1d 6292 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = z -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
206205oveq2d 6293 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) )
207206fveq1d 5850 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
208207neeq1d 2680 . . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) ) )
209202, 208imbi12d 318 . . . . . . . . . . . . . . . . . . . 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 2041 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) )
21146hausflf2 20789 . . . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) ~~ 1o )
213 en1b 7620 . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. (TopOn ` B ) )
217 flfval 20781 . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ) )
219218adantr 463 . . . . . . . . . . . . . . . . 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 6578 . . . . . . . . . . . . . . . . . . . . . 22 |- ( K e. Haus -> U. K e. _V )
22132, 220syl 17 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U. K e. _V )
222221ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> U. K e. _V )
22346, 222syl5eqel 2494 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> B e. _V )
224199adantr 463 . . . . . . . . . . . . . . . . . . . 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 20639 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( fBas ` A ) )
226224, 225syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( fBas ` A ) )
22737ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> F : A --> B )
228 simpr 459 . . . . . . . . . . . . . . . . . . . 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 20666 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
230199, 229syl 17 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
231230adantr 463 . . . . . . . . . . . . . . . . . . . 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 2493 . . . . . . . . . . . . . . . . . . 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 2402 . . . . . . . . . . . . . . . . . . . 20 |- ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) )
234233imaelfm 20742 . . . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . . . 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 20769 . . . . . . . . . . . . . . . . . 18 |- ( ( F " ( v i^i A ) ) e. ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ) C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
237235, 236syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ) C_ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
238219, 237eqsstrd 3475 . . . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . 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 5858 . . . . . . . . . . . . . . . . 17 |- ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
241240uniex 6577 . . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
242241snss 4095 . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . 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 1229 . . . . . . . . . . . 12 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
246245adantlr 713 . . . . . . . . . . 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 3442 . . . . . . . . . 10 |- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. w )
248247ralrimiva 2817 . . . . . . . . 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 616 . . . . . . . 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 2877 . . . . . . 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 724 . . . . . 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 20856 . . . . . . . . . 10 |- ( ph -> ( ( JCnExt K ) ` F ) : C --> B )
254 ffun 5715 . . . . . . . . . 10 |- ( ( ( JCnExt K ) ` F ) : C --> B -> Fun ( ( JCnExt K ) ` F ) )
255253, 254syl 17 . . . . . . . . 9 |- ( ph -> Fun ( ( JCnExt K ) ` F ) )
256255adantr 463 . . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> Fun ( ( JCnExt K ) ` F ) )
25765neii1 19898 . . . . . . . . . 10 |- ( ( J e. Top /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
2584, 257sylan 469 . . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
259 fdm 5717 . . . . . . . . . . 11 |- ( ( ( JCnExt K ) ` F ) : C --> B -> dom ( ( JCnExt K ) ` F ) = C )
260253, 259syl 17 . . . . . . . . . 10 |- ( ph -> dom ( ( JCnExt K ) ` F ) = C )
261260adantr 463 . . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> dom ( ( JCnExt K ) ` F ) = C )
262258, 261sseqtr4d 3478 . . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( JCnExt K ) ` F ) )
263 funimass4 5899 . . . . . . . 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 659 . . . . . . 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 2878 . . . . 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 2817 . . 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 2817 . 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 20074 . . 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 1230 . 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 367   /\ w3a 974   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2753   E.wrex 2754   _Vcvv 3058   i^i cin 3412   C_ wss 3413   (/)c0 3737   {csn 3971   U.cuni 4190   class class class wbr 4394   dom cdm 4822   ran crn 4823   "cima 4825   Fun wfun 5562   -->wf 5564   ` cfv 5568  (class class class)co 6277   1oc1o 7159   ~~ cen 7550   ↾t crest 15033   fBascfbas 18724   filGencfg 18725   Topctop 19684  TopOnctopon 19685   clsccl 19809   neicnei 19889   Cn ccn 20016   Hauscha 20100   Regcreg 20101   Filcfil 20636   FilMap cfm 20724   fLim cflim 20725   fLimf cflf 20726  CnExtccnext 20849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6783  df-2nd 6784  df-1o 7166  df-map 7458  df-pm 7459  df-en 7554  df-rest 15035  df-topgen 15056  df-fbas 18734  df-fg 18735  df-top 19689  df-topon 19692  df-cld 19810  df-ntr 19811  df-cls 19812  df-nei 19890  df-cn 20019  df-cnp 20020  df-haus 20107  df-reg 20108  df-fil 20637  df-fm 20729  df-flim 20730  df-flf 20731  df-cnext 20850
This theorem is referenced by:  cnextucn  21096
  Copyright terms: Public domain W3C validator