Metamath Proof Explorer


Theorem cnextcn

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)

Ref Expression
Hypotheses 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 cnextcn
|- ( ph -> ( ( J CnExt K ) ` F ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 cnextf.1
 |-  C = U. J
2 cnextf.2
 |-  B = U. K
3 cnextf.3
 |-  ( ph -> J e. Top )
4 cnextf.4
 |-  ( ph -> K e. Haus )
5 cnextf.5
 |-  ( ph -> F : A --> B )
6 cnextf.a
 |-  ( ph -> A C_ C )
7 cnextf.6
 |-  ( ph -> ( ( cls ` J ) ` A ) = C )
8 cnextf.7
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) )
9 cnextcn.8
 |-  ( ph -> K e. Reg )
10 simpll
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> ph )
11 simpll
 |-  ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ph )
12 simpr3
 |-  ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 )
13 3 ad2antrr
 |-  ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> J e. Top )
14 simpr2
 |-  ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> d e. ( ( nei ` J ) ` { x } ) )
15 neii2
 |-  ( ( J e. Top /\ d e. ( ( nei ` J ) ` { x } ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) )
16 13 14 15 syl2anc
 |-  ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 ) )
17 vex
 |-  x e. _V
18 17 snss
 |-  ( x e. v <-> { x } C_ v )
19 18 biimpri
 |-  ( { x } C_ v -> x e. v )
20 19 anim1i
 |-  ( ( { x } C_ v /\ v C_ d ) -> ( x e. v /\ v C_ d ) )
21 20 anim2i
 |-  ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
22 21 anim2i
 |-  ( ( ph /\ ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
23 22 ex
 |-  ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) )
24 3anass
 |-  ( ( ph /\ v e. J /\ x e. v ) <-> ( ph /\ ( v e. J /\ x e. v ) ) )
25 24 anbi1i
 |-  ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) )
26 anass
 |-  ( ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) <-> ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) )
27 anass
 |-  ( ( ( v e. J /\ x e. v ) /\ v C_ d ) <-> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
28 27 anbi2i
 |-  ( ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
29 25 26 28 3bitri
 |-  ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
30 opnneip
 |-  ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
31 3 30 syl3an1
 |-  ( ( ph /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
32 31 adantr
 |-  ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> v e. ( ( nei ` J ) ` { x } ) )
33 simpr2
 |-  ( ( v C_ d /\ ( ph /\ v e. J /\ x e. v ) ) -> v e. J )
34 33 ex
 |-  ( v C_ d -> ( ( ph /\ v e. J /\ x e. v ) -> v e. J ) )
35 34 imdistanri
 |-  ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. J /\ v C_ d ) )
36 32 35 jca
 |-  ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) )
37 29 36 sylbir
 |-  ( ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) )
38 23 37 syl6
 |-  ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) )
39 38 adantr
 |-  ( ( 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 ) ) ) )
40 haustop
 |-  ( K e. Haus -> K e. Top )
41 4 40 syl
 |-  ( ph -> K e. Top )
42 imassrn
 |-  ( F " ( d i^i A ) ) C_ ran F
43 5 frnd
 |-  ( ph -> ran F C_ B )
44 42 43 sstrid
 |-  ( ph -> ( F " ( d i^i A ) ) C_ B )
45 ssrin
 |-  ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) )
46 imass2
 |-  ( ( v i^i A ) C_ ( d i^i A ) -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
47 45 46 syl
 |-  ( v C_ d -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
48 2 clsss
 |-  ( ( 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 ) ) ) )
49 41 44 47 48 syl2an3an
 |-  ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
50 sstr
 |-  ( ( ( ( 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 )
51 49 50 sylan
 |-  ( ( ( ph /\ v C_ d ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
52 51 an32s
 |-  ( ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
53 52 ex
 |-  ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( v C_ d -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
54 53 anim2d
 |-  ( ( 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 ) ) )
55 54 anim2d
 |-  ( ( 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 ) ) ) )
56 39 55 syld
 |-  ( ( 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 ) ) ) )
57 56 reximdv2
 |-  ( ( 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 ) ) )
58 57 imp
 |-  ( ( ( 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 ) )
59 11 12 16 58 syl21anc
 |-  ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 59 3anassrs
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 ) )
61 simpr
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
62 simp-4l
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> ph )
63 simplr
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) /\ ( ( cls ` K ) ` ( F " u ) ) C_ w ) -> u e. ( ( ( nei ` J ) ` { x } ) |`t A ) )
64 imaeq2
 |-  ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) )
65 64 fveq2d
 |-  ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
66 65 sseq1d
 |-  ( u = ( d i^i A ) -> ( ( ( cls ` K ) ` ( F " u ) ) C_ w <-> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
67 66 biimpcd
 |-  ( ( ( cls ` K ) ` ( F " u ) ) C_ w -> ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
68 67 reximdv
 |-  ( ( ( 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 ) )
69 fvexd
 |-  ( ph -> ( ( nei ` J ) ` { x } ) e. _V )
70 1 toptopon
 |-  ( J e. Top <-> J e. ( TopOn ` C ) )
71 3 70 sylib
 |-  ( ph -> J e. ( TopOn ` C ) )
72 71 elfvexd
 |-  ( ph -> C e. _V )
73 72 6 ssexd
 |-  ( ph -> A e. _V )
74 elrest
 |-  ( ( ( ( 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 ) ) )
75 69 73 74 syl2anc
 |-  ( ph -> ( u e. ( ( ( nei ` J ) ` { x } ) |`t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) )
76 75 biimpa
 |-  ( ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ) -> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) )
77 68 76 impel
 |-  ( ( ( ( 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 )
78 61 62 63 77 syl12anc
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 )
79 eleq1w
 |-  ( x = y -> ( x e. C <-> y e. C ) )
80 79 anbi2d
 |-  ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
81 sneq
 |-  ( x = y -> { x } = { y } )
82 81 fveq2d
 |-  ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
83 82 oveq1d
 |-  ( x = y -> ( ( ( nei ` J ) ` { x } ) |`t A ) = ( ( ( nei ` J ) ` { y } ) |`t A ) )
84 83 oveq2d
 |-  ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) )
85 84 fveq1d
 |-  ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) )
86 85 neeq1d
 |-  ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) ) )
87 80 86 imbi12d
 |-  ( 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 ) =/= (/) ) ) )
88 87 8 chvarvv
 |-  ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) |`t A ) ) ` F ) =/= (/) )
89 1 2 3 4 5 6 7 88 cnextfvval
 |-  ( ( ph /\ x e. C ) -> ( ( ( J CnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
90 fvex
 |-  ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. _V
91 90 uniex
 |-  U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. _V
92 91 snid
 |-  U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) }
93 4 adantr
 |-  ( ( ph /\ x e. C ) -> K e. Haus )
94 7 eleq2d
 |-  ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
95 94 biimpar
 |-  ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
96 71 adantr
 |-  ( ( ph /\ x e. C ) -> J e. ( TopOn ` C ) )
97 6 adantr
 |-  ( ( ph /\ x e. C ) -> A C_ C )
98 simpr
 |-  ( ( ph /\ x e. C ) -> x e. C )
99 trnei
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
100 96 97 98 99 syl3anc
 |-  ( ( ph /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
101 95 100 mpbid
 |-  ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
102 5 adantr
 |-  ( ( ph /\ x e. C ) -> F : A --> B )
103 2 hausflf2
 |-  ( ( ( 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 )
104 93 101 102 8 103 syl31anc
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ~~ 1o )
105 en1b
 |-  ( ( ( 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 ) } )
106 104 105 sylib
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) } )
107 92 106 eleqtrrid
 |-  ( ( ph /\ x e. C ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
108 89 107 eqeltrd
 |-  ( ( ph /\ x e. C ) -> ( ( ( J CnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
109 2 toptopon
 |-  ( K e. Top <-> K e. ( TopOn ` B ) )
110 41 109 sylib
 |-  ( ph -> K e. ( TopOn ` B ) )
111 110 adantr
 |-  ( ( ph /\ x e. C ) -> K e. ( TopOn ` B ) )
112 flfnei
 |-  ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) <-> ( ( ( ( J CnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) ) )
113 111 101 102 112 syl3anc
 |-  ( ( ph /\ x e. C ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) <-> ( ( ( ( J CnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) ) )
114 108 113 mpbid
 |-  ( ( ph /\ x e. C ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b ) )
115 114 simprd
 |-  ( ( ph /\ x e. C ) -> A. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b )
116 115 r19.21bi
 |-  ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b )
117 116 ad4ant13
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( F " u ) C_ b )
118 41 ad3antrrr
 |-  ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> K e. Top )
119 simplr
 |-  ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) )
120 2 neii1
 |-  ( ( K e. Top /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> b C_ B )
121 118 119 120 syl2anc
 |-  ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b C_ B )
122 simpr
 |-  ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
123 2 clsss
 |-  ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) )
124 sstr
 |-  ( ( ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
125 123 124 sylan
 |-  ( ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
126 125 3an1rs
 |-  ( ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
127 126 ex
 |-  ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( F " u ) C_ b -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) )
128 127 reximdv
 |-  ( ( 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 ) )
129 118 121 122 128 syl3anc
 |-  ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 ) )
130 129 adantllr
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 ) )
131 117 130 mpd
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w )
132 41 ad2antrr
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> K e. Top )
133 9 ad2antrr
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> K e. Reg )
134 133 ad2antrr
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> K e. Reg )
135 simplr
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> c e. K )
136 simprl
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( ( ( J CnExt K ) ` F ) ` x ) e. c )
137 regsep
 |-  ( ( K e. Reg /\ c e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. c ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) )
138 134 135 136 137 syl3anc
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) )
139 sstr
 |-  ( ( ( ( cls ` K ) ` b ) C_ c /\ c C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
140 139 expcom
 |-  ( c C_ w -> ( ( ( cls ` K ) ` b ) C_ c -> ( ( cls ` K ) ` b ) C_ w ) )
141 140 anim2d
 |-  ( c C_ w -> ( ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) )
142 141 reximdv
 |-  ( c C_ w -> ( E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) )
143 142 ad2antll
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ c ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) )
144 138 143 mpd
 |-  ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) )
145 simpr
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) )
146 neii2
 |-  ( ( K e. Top /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) )
147 fvex
 |-  ( ( ( J CnExt K ) ` F ) ` x ) e. _V
148 147 snss
 |-  ( ( ( ( J CnExt K ) ` F ) ` x ) e. c <-> { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c )
149 148 anbi1i
 |-  ( ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) <-> ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) )
150 149 biimpri
 |-  ( ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
151 150 reximi
 |-  ( E. c e. K ( { ( ( ( J CnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> E. c e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
152 146 151 syl
 |-  ( ( K e. Top /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
153 132 145 152 syl2anc
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. c e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
154 144 153 r19.29a
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) )
155 anass
 |-  ( ( ( b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) /\ ( ( cls ` K ) ` b ) C_ w ) <-> ( b e. K /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) )
156 opnneip
 |-  ( ( K e. Top /\ b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) )
157 156 3expib
 |-  ( K e. Top -> ( ( b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) )
158 157 anim1d
 |-  ( K e. Top -> ( ( ( b e. K /\ ( ( ( J CnExt K ) ` F ) ` x ) e. b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ ( ( cls ` K ) ` b ) C_ w ) ) )
159 155 158 syl5bir
 |-  ( K e. Top -> ( ( b e. K /\ ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) -> ( b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) /\ ( ( cls ` K ) ` b ) C_ w ) ) )
160 159 reximdv2
 |-  ( K e. Top -> ( E. b e. K ( ( ( ( J CnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) -> E. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ( ( cls ` K ) ` b ) C_ w ) )
161 132 154 160 sylc
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. b e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ( ( cls ` K ) ` b ) C_ w )
162 131 161 r19.29a
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. u e. ( ( ( nei ` J ) ` { x } ) |`t A ) ( ( cls ` K ) ` ( F " u ) ) C_ w )
163 78 162 r19.29a
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. d e. ( ( nei ` J ) ` { x } ) ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w )
164 60 163 r19.29a
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
165 simplr
 |-  ( ( ( ( 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 )
166 simpll
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph )
167 3 ad2antrr
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> J e. Top )
168 simplr
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. J )
169 1 eltopss
 |-  ( ( J e. Top /\ v e. J ) -> v C_ C )
170 167 168 169 syl2anc
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> v C_ C )
171 simpr
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. v )
172 170 171 sseldd
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C )
173 fvexd
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( nei ` J ) ` { z } ) e. _V )
174 73 ad2antrr
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> A e. _V )
175 opnneip
 |-  ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
176 3 175 syl3an1
 |-  ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
177 176 3expa
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
178 elrestr
 |-  ( ( ( ( nei ` J ) ` { z } ) e. _V /\ A e. _V /\ v e. ( ( nei ` J ) ` { z } ) ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) )
179 173 174 177 178 syl3anc
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) )
180 1 2 3 4 5 6 7 8 cnextfvval
 |-  ( ( ph /\ z e. C ) -> ( ( ( J CnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) )
181 180 adantr
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( J CnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) )
182 4 adantr
 |-  ( ( ph /\ z e. C ) -> K e. Haus )
183 7 eleq2d
 |-  ( ph -> ( z e. ( ( cls ` J ) ` A ) <-> z e. C ) )
184 183 biimpar
 |-  ( ( ph /\ z e. C ) -> z e. ( ( cls ` J ) ` A ) )
185 71 adantr
 |-  ( ( ph /\ z e. C ) -> J e. ( TopOn ` C ) )
186 6 adantr
 |-  ( ( ph /\ z e. C ) -> A C_ C )
187 simpr
 |-  ( ( ph /\ z e. C ) -> z e. C )
188 trnei
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) ) )
189 185 186 187 188 syl3anc
 |-  ( ( ph /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) ) )
190 184 189 mpbid
 |-  ( ( ph /\ z e. C ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) )
191 5 adantr
 |-  ( ( ph /\ z e. C ) -> F : A --> B )
192 eleq1w
 |-  ( x = z -> ( x e. C <-> z e. C ) )
193 192 anbi2d
 |-  ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) )
194 sneq
 |-  ( x = z -> { x } = { z } )
195 194 fveq2d
 |-  ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
196 195 oveq1d
 |-  ( x = z -> ( ( ( nei ` J ) ` { x } ) |`t A ) = ( ( ( nei ` J ) ` { z } ) |`t A ) )
197 196 oveq2d
 |-  ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) )
198 197 fveq1d
 |-  ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) )
199 198 neeq1d
 |-  ( x = z -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) =/= (/) ) )
200 193 199 imbi12d
 |-  ( 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 ) =/= (/) ) ) )
201 200 8 chvarvv
 |-  ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) =/= (/) )
202 2 hausflf2
 |-  ( ( ( 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 )
203 182 190 191 201 202 syl31anc
 |-  ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) ~~ 1o )
204 en1b
 |-  ( ( ( 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 ) } )
205 203 204 sylib
 |-  ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) } )
206 205 adantr
 |-  ( ( ( 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 ) } )
207 110 adantr
 |-  ( ( ph /\ z e. C ) -> K e. ( TopOn ` B ) )
208 flfval
 |-  ( ( 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 ) ) ) )
209 207 190 191 208 syl3anc
 |-  ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) |`t A ) ) ) )
210 209 adantr
 |-  ( ( ( 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 ) ) ) )
211 4 uniexd
 |-  ( ph -> U. K e. _V )
212 211 ad2antrr
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> U. K e. _V )
213 2 212 eqeltrid
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> B e. _V )
214 190 adantr
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) )
215 filfbas
 |-  ( ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( fBas ` A ) )
216 214 215 syl
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( fBas ` A ) )
217 5 ad2antrr
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> F : A --> B )
218 simpr
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) )
219 fgfil
 |-  ( ( ( ( nei ` J ) ` { z } ) |`t A ) e. ( Fil ` A ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( ( ( nei ` J ) ` { z } ) |`t A ) )
220 190 219 syl
 |-  ( ( ph /\ z e. C ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( ( ( nei ` J ) ` { z } ) |`t A ) )
221 220 adantr
 |-  ( ( ( 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 ) )
222 218 221 eleqtrrd
 |-  ( ( ( 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 ) ) )
223 eqid
 |-  ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) |`t A ) )
224 223 imaelfm
 |-  ( ( ( 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 ) ) )
225 213 216 217 222 224 syl31anc
 |-  ( ( ( 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 ) ) )
226 flimclsi
 |-  ( ( 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 ) ) ) )
227 225 226 syl
 |-  ( ( ( 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 ) ) ) )
228 210 227 eqsstrd
 |-  ( ( ( 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 ) ) ) )
229 206 228 eqsstrrd
 |-  ( ( ( 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 ) ) ) )
230 fvex
 |-  ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) e. _V
231 230 uniex
 |-  U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) |`t A ) ) ` F ) e. _V
232 231 snss
 |-  ( 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 ) ) ) )
233 229 232 sylibr
 |-  ( ( ( 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 ) ) ) )
234 181 233 eqeltrd
 |-  ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) |`t A ) ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
235 166 172 179 234 syl21anc
 |-  ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
236 235 adantlr
 |-  ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
237 165 236 sseldd
 |-  ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( J CnExt K ) ` F ) ` z ) e. w )
238 237 ralrimiva
 |-  ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w )
239 238 expl
 |-  ( ph -> ( ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) )
240 239 reximdv
 |-  ( 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 ( ( ( J CnExt K ) ` F ) ` z ) e. w ) )
241 240 ad2antrr
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt 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 ( ( ( J CnExt K ) ` F ) ` z ) e. w ) )
242 164 241 mpd
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w )
243 1 2 3 4 5 6 7 8 cnextf
 |-  ( ph -> ( ( J CnExt K ) ` F ) : C --> B )
244 243 ffund
 |-  ( ph -> Fun ( ( J CnExt K ) ` F ) )
245 244 adantr
 |-  ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> Fun ( ( J CnExt K ) ` F ) )
246 1 neii1
 |-  ( ( J e. Top /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
247 3 246 sylan
 |-  ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
248 243 fdmd
 |-  ( ph -> dom ( ( J CnExt K ) ` F ) = C )
249 248 adantr
 |-  ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> dom ( ( J CnExt K ) ` F ) = C )
250 247 249 sseqtrrd
 |-  ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( J CnExt K ) ` F ) )
251 funimass4
 |-  ( ( Fun ( ( J CnExt K ) ` F ) /\ v C_ dom ( ( J CnExt K ) ` F ) ) -> ( ( ( ( J CnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) )
252 245 250 251 syl2anc
 |-  ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( ( ( ( J CnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w ) )
253 252 biimprd
 |-  ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w -> ( ( ( J CnExt K ) ` F ) " v ) C_ w ) )
254 253 reximdva
 |-  ( ph -> ( E. v e. ( ( nei ` J ) ` { x } ) A. z e. v ( ( ( J CnExt K ) ` F ) ` z ) e. w -> E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) )
255 10 242 254 sylc
 |-  ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) ) -> E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w )
256 255 ralrimiva
 |-  ( ( ph /\ x e. C ) -> A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w )
257 256 ralrimiva
 |-  ( ph -> A. x e. C A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w )
258 1 2 cnnei
 |-  ( ( J e. Top /\ K e. Top /\ ( ( J CnExt K ) ` F ) : C --> B ) -> ( ( ( J CnExt K ) ` F ) e. ( J Cn K ) <-> A. x e. C A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) )
259 3 41 243 258 syl3anc
 |-  ( ph -> ( ( ( J CnExt K ) ` F ) e. ( J Cn K ) <-> A. x e. C A. w e. ( ( nei ` K ) ` { ( ( ( J CnExt K ) ` F ) ` x ) } ) E. v e. ( ( nei ` J ) ` { x } ) ( ( ( J CnExt K ) ` F ) " v ) C_ w ) )
260 257 259 mpbird
 |-  ( ph -> ( ( J CnExt K ) ` F ) e. ( J Cn K ) )