This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrid 
 |-  ( 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 ) )