Theorem cnextcn 21082

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.

Step	Hyp	Ref	Expression
1		simpll 760	. . . . 5 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> ph )
2		simpll 760	. . . . . . . . 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 1016	. . . . . . . . 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 )
5	4	ad2antrr 732	. . . . . . . . . 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 1015	. . . . . . . . . 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 20124	. . . . . . . . . 10 |- ( ( J e. Top /\ d e. ( ( nei ` J ) ` { x } ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) )
8	5, 6, 7	syl2anc 667	. . . . . . . . 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 3048	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
10	9	snss 4096	. . . . . . . . . . . . . . . . . . 19 |- ( x e. v <-> { x } C_ v )
11	10	biimpri 210	. . . . . . . . . . . . . . . . . 18 |- ( { x } C_ v -> x e. v )
12	11	anim1i 572	. . . . . . . . . . . . . . . . 17 |- ( ( { x } C_ v /\ v C_ d ) -> ( x e. v /\ v C_ d ) )
13	12	anim2i 573	. . . . . . . . . . . . . . . 16 |- ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
14	13	anim2i 573	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
15	14	ex 436	. . . . . . . . . . . . . 14 |- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) )
16		3anass 989	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) <-> ( ph /\ ( v e. J /\ x e. v ) ) )
17	16	anbi1i 701	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) )
18		anass 655	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) <-> ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) )
19		anass 655	. . . . . . . . . . . . . . . . 17 |- ( ( ( v e. J /\ x e. v ) /\ v C_ d ) <-> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
20	19	anbi2i 700	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
21	17, 18, 20	3bitri 275	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
22		opnneip 20135	. . . . . . . . . . . . . . . . . 18 |- ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
23	4, 22	syl3an1 1301	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
24	23	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> v e. ( ( nei ` J ) ` { x } ) )
25		simpr2 1015	. . . . . . . . . . . . . . . . . 18 |- ( ( v C_ d /\ ( ph /\ v e. J /\ x e. v ) ) -> v e. J )
26	25	ex 436	. . . . . . . . . . . . . . . . 17 |- ( v C_ d -> ( ( ph /\ v e. J /\ x e. v ) -> v e. J ) )
27	26	imdistanri 697	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. J /\ v C_ d ) )
28	24, 27	jca 535	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) )
29	21, 28	sylbir 217	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) )
30	15, 29	syl6 34	. . . . . . . . . . . . 13 |- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. ( ( nei ` J ) ` { x } ) /\ ( v e. J /\ v C_ d ) ) ) )
31	30	adantr 467	. . . . . . . . . . . 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 20347	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. Haus -> K e. Top )
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. Top )
35	34	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> K e. Top )
36		imassrn 5179	. . . . . . . . . . . . . . . . . . . 20 |- ( F " ( d i^i A ) ) C_ ran F
37		cnextf.5	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F : A --> B )
38		frn 5735	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : A --> B -> ran F C_ B )
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran F C_ B )
40	36, 39	syl5ss 3443	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( F " ( d i^i A ) ) C_ B )
41	40	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> ( F " ( d i^i A ) ) C_ B )
42		ssrin 3657	. . . . . . . . . . . . . . . . . . . 20 |- ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) )
43		imass2 5204	. . . . . . . . . . . . . . . . . . . 20 |- ( ( v i^i A ) C_ ( d i^i A ) -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
44	42, 43	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( v C_ d -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
45	44	adantl 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
46		cnextf.2	. . . . . . . . . . . . . . . . . . 19 |- B = U. K
47	46	clsss 20069	. . . . . . . . . . . . . . . . . 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 ) ) ) )
48	35, 41, 45, 47	syl3anc 1268	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
49		sstr 3440	. . . . . . . . . . . . . . . . 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 )
50	48, 49	sylan 474	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v C_ d ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
51	50	an32s 813	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w )
52	51	ex 436	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) -> ( v C_ d -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) )
53	52	anim2d 569	. . . . . . . . . . . . 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 ) ) )
54	53	anim2d 569	. . . . . . . . . . . 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 ) ) ) )
55	31, 54	syld 45	. . . . . . . . . . 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 ) ) ) )
56	55	reximdv2 2858	. . . . . . . . . 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 ) ) )
57	56	imp 431	. . . . . . . . 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 ) )
58	2, 3, 8, 57	syl21anc 1267	. . . . . . . 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 ) )
59	58	3anassrs 1232	. . . . . . 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 463	. . . . . . . . 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 776	. . . . . . . . 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 762	. . . . . . . . 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 5875	. . . . . . . . . . . . . 14 |- ( ( nei ` J ) ` { x } ) e. _V
64	63	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( nei ` J ) ` { x } ) e. _V )
65		cnextf.1	. . . . . . . . . . . . . . . . 17 |- C = U. J
66	65	toptopon 19948	. . . . . . . . . . . . . . . 16 |- ( J e. Top <-> J e. (TopOn ` C ) )
67	4, 66	sylib 200	. . . . . . . . . . . . . . 15 |- ( ph -> J e. (TopOn ` C ) )
68	67	elfvexd 5893	. . . . . . . . . . . . . 14 |- ( ph -> C e. _V )
69		cnextf.a	. . . . . . . . . . . . . 14 |- ( ph -> A C_ C )
70	68, 69	ssexd 4550	. . . . . . . . . . . . 13 |- ( ph -> A e. _V )
71		elrest 15326	. . . . . . . . . . . . 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 ) ) )
72	64, 70, 71	syl2anc 667	. . . . . . . . . . . 12 |- ( ph -> ( u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) )
73	72	biimpa 487	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) -> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) )
74		imaeq2 5164	. . . . . . . . . . . . . . 15 |- ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) )
75	74	fveq2d 5869	. . . . . . . . . . . . . 14 |- ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
76	75	sseq1d 3459	. . . . . . . . . . . . 13 |- ( u = ( d i^i A ) -> ( ( ( cls ` K ) ` ( F " u ) ) C_ w <-> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
77	76	biimpcd 228	. . . . . . . . . . . 12 |- ( ( ( cls ` K ) ` ( F " u ) ) C_ w -> ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
78	77	reximdv 2861	. . . . . . . . . . 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 ) )
79	73, 78	syl5 33	. . . . . . . . . 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 ) )
80	79	imp 431	. . . . . . . . 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 )
81	60, 61, 62, 80	syl12anc 1266	. . . . . . . 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 768	. . . . . . . . . . 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 762	. . . . . . . . . . 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 2517	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( x e. C <-> y e. C ) )
86	85	anbi2d 710	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
87		sneq 3978	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> { x } = { y } )
88	87	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
89	88	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { y } ) ↾t A ) )
90	89	oveq2d 6306	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) )
91	90	fveq1d 5867	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) )
92	91	neeq1d 2683	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) ) )
93	86, 92	imbi12d 322	. . . . . . . . . . . . . . . . 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 ) =/= (/) )
95	93, 94	chvarv 2107	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) )
96	65, 46, 4, 32, 37, 69, 84, 95	cnextfvval 21080	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
97		fvex 5875	. . . . . . . . . . . . . . . . . 18 |- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
98	97	uniex 6587	. . . . . . . . . . . . . . . . 17 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
99	98	snid 3996	. . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) }
100	32	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> K e. Haus )
101	84	eleq2d 2514	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
102	101	biimpar 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
103	67	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> J e. (TopOn ` C ) )
104	69	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> A C_ C )
105		simpr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> x e. C )
106		trnei 20907	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J e. (TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) ) )
107	103, 104, 105, 106	syl3anc 1268	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) ) )
108	102, 107	mpbid 214	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) )
109	37	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> F : A --> B )
110	46	hausflf2 21013	. . . . . . . . . . . . . . . . . 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 )
111	100, 108, 109, 94, 110	syl31anc 1271	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ~~ 1o )
112		en1b 7637	. . . . . . . . . . . . . . . . 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 ) } )
113	111, 112	sylib 200	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) } )
114	99, 113	syl5eleqr 2536	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
115	96, 114	eqeltrd 2529	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
116	46	toptopon 19948	. . . . . . . . . . . . . . . . 17 |- ( K e. Top <-> K e. (TopOn ` B ) )
117	34, 116	sylib 200	. . . . . . . . . . . . . . . 16 |- ( ph -> K e. (TopOn ` B ) )
118	117	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> K e. (TopOn ` B ) )
119		flfnei 21006	. . . . . . . . . . . . . . 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 ) ) )
120	118, 108, 109, 119	syl3anc 1268	. . . . . . . . . . . . . 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 ) ) )
121	115, 120	mpbid 214	. . . . . . . . . . . . 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 ) )
122	121	simprd 465	. . . . . . . . . . . 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 )
123	122	r19.21bi 2757	. . . . . . . . . . 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 )
124	82, 83, 123	syl2anc 667	. . . . . . . . . 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 )
125	34	ad3antrrr 736	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> K e. Top )
126		simplr 762	. . . . . . . . . . . . 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 ) } ) )
127	46	neii1 20122	. . . . . . . . . . . . 13 |- ( ( K e. Top /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> b C_ B )
128	125, 126, 127	syl2anc 667	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b C_ B )
129		simpr 463	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
130	46	clsss 20069	. . . . . . . . . . . . . . . 16 |- ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) )
131		sstr 3440	. . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
132	130, 131	sylan 474	. . . . . . . . . . . . . . 15 |- ( ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
133	132	3an1rs 1221	. . . . . . . . . . . . . 14 |- ( ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
134	133	ex 436	. . . . . . . . . . . . 13 |- ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( F " u ) C_ b -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) )
135	134	reximdv 2861	. . . . . . . . . . . 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 ) )
136	125, 128, 129, 135	syl3anc 1268	. . . . . . . . . . 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 ) )
137	136	adantllr 725	. . . . . . . . . 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 ) )
138	124, 137	mpd 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 )
139	34	ad2antrr 732	. . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Top )
140		cnextcn.8	. . . . . . . . . . . . . . 15 |- ( ph -> K e. Reg )
141	140	ad2antrr 732	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Reg )
142	141	ad2antrr 732	. . . . . . . . . . . . 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 762	. . . . . . . . . . . . 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 764	. . . . . . . . . . . . 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 20350	. . . . . . . . . . . . 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 ) )
146	142, 143, 144, 145	syl3anc 1268	. . . . . . . . . . . 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 3440	. . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` b ) C_ c /\ c C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
148	147	expcom 437	. . . . . . . . . . . . . . 15 |- ( c C_ w -> ( ( ( cls ` K ) ` b ) C_ c -> ( ( cls ` K ) ` b ) C_ w ) )
149	148	anim2d 569	. . . . . . . . . . . . . 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 ) ) )
150	149	reximdv 2861	. . . . . . . . . . . . 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 ) ) )
151	150	ad2antll 735	. . . . . . . . . . . 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 ) ) )
152	146, 151	mpd 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 463	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
154		neii2 20124	. . . . . . . . . . . . 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 5875	. . . . . . . . . . . . . . . . 17 |- ( ( ( JCnExt K ) ` F ) ` x ) e. _V
156	155	snss 4096	. . . . . . . . . . . . . . . 16 |- ( ( ( ( JCnExt K ) ` F ) ` x ) e. c <-> { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c )
157	156	anbi1i 701	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) <-> ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) )
158	157	biimpri 210	. . . . . . . . . . . . . 14 |- ( ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
159	158	reximi 2855	. . . . . . . . . . . . 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 ) )
160	154, 159	syl 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 ) )
161	139, 153, 160	syl2anc 667	. . . . . . . . . . 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 ) )
162	152, 161	r19.29a 2932	. . . . . . . . . 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 655	. . . . . . . . . . . 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 20135	. . . . . . . . . . . . . 14 |- ( ( K e. Top /\ b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
165	164	3expib 1211	. . . . . . . . . . . . 13 |- ( K e. Top -> ( ( b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) )
166	165	anim1d 568	. . . . . . . . . . . 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 ) ) )
167	163, 166	syl5bir 222	. . . . . . . . . . 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 ) ) )
168	167	reximdv2 2858	. . . . . . . . . 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 ) )
169	139, 162, 168	sylc 62	. . . . . . . . 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 )
170	138, 169	r19.29a 2932	. . . . . . . 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 )
171	81, 170	r19.29a 2932	. . . . . . 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 )
172	59, 171	r19.29a 2932	. . . . . 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 762	. . . . . . . . . . 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 760	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph )
175	4	ad2antrr 732	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> J e. Top )
176		simplr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. J )
177	65	eltopss 19937	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ v e. J ) -> v C_ C )
178	175, 176, 177	syl2anc 667	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v C_ C )
179		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. v )
180	178, 179	sseldd 3433	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C )
181		fvex 5875	. . . . . . . . . . . . . . 15 |- ( ( nei ` J ) ` { z } ) e. _V
182	181	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( nei ` J ) ` { z } ) e. _V )
183	70	ad2antrr 732	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> A e. _V )
184		opnneip 20135	. . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
185	4, 184	syl3an1 1301	. . . . . . . . . . . . . . 15 |- ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
186	185	3expa 1208	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
187		elrestr 15327	. . . . . . . . . . . . . 14 |- ( ( ( ( nei ` J ) ` { z } ) e. _V /\ A e. _V /\ v e. ( ( nei ` J ) ` { z } ) ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) )
188	182, 183, 186, 187	syl3anc 1268	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) )
189	65, 46, 4, 32, 37, 69, 84, 94	cnextfvval 21080	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. C ) -> ( ( ( JCnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
190	189	adantr 467	. . . . . . . . . . . . . 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 ) )
191	32	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. Haus )
192	84	eleq2d 2514	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( z e. ( ( cls ` J ) ` A ) <-> z e. C ) )
193	192	biimpar 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> z e. ( ( cls ` J ) ` A ) )
194	67	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> J e. (TopOn ` C ) )
195	69	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> A C_ C )
196		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> z e. C )
197		trnei 20907	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( J e. (TopOn ` C ) /\ A C_ C /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) ) )
198	194, 195, 196, 197	syl3anc 1268	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) ) )
199	193, 198	mpbid 214	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) )
200	37	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> F : A --> B )
201		eleq1 2517	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x e. C <-> z e. C ) )
202	201	anbi2d 710	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) )
203		sneq 3978	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = z -> { x } = { z } )
204	203	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
205	204	oveq1d 6305	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = z -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
206	205	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) )
207	206	fveq1d 5867	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
208	207	neeq1d 2683	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) ) )
209	202, 208	imbi12d 322	. . . . . . . . . . . . . . . . . . . 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 ) =/= (/) ) ) )
210	209, 94	chvarv 2107	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) )
211	46	hausflf2 21013	. . . . . . . . . . . . . . . . . . 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 )
212	191, 199, 200, 210, 211	syl31anc 1271	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) ~~ 1o )
213		en1b 7637	. . . . . . . . . . . . . . . . . 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 ) } )
214	212, 213	sylib 200	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) } )
215	214	adantr 467	. . . . . . . . . . . . . . . 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 ) } )
216	117	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. (TopOn ` B ) )
217		flfval 21005	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
218	216, 199, 200, 217	syl3anc 1268	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ) )
219	218	adantr 467	. . . . . . . . . . . . . . . . 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 6588	. . . . . . . . . . . . . . . . . . . . . 22 |- ( K e. Haus -> U. K e. _V )
221	32, 220	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U. K e. _V )
222	221	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> U. K e. _V )
223	46, 222	syl5eqel 2533	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> B e. _V )
224	199	adantr 467	. . . . . . . . . . . . . . . . . . . 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 20863	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( fBas ` A ) )
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( fBas ` A ) )
227	37	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> F : A --> B )
228		simpr 463	. . . . . . . . . . . . . . . . . . . 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 20890	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
230	199, 229	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
231	230	adantr 467	. . . . . . . . . . . . . . . . . . . 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 ) )
232	228, 231	eleqtrrd 2532	. . . . . . . . . . . . . . . . . . 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 2451	. . . . . . . . . . . . . . . . . . . 20 |- ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) )
234	233	imaelfm 20966	. . . . . . . . . . . . . . . . . . 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 ) ) )
235	223, 226, 227, 232, 234	syl31anc 1271	. . . . . . . . . . . . . . . . . 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 20993	. . . . . . . . . . . . . . . . . 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 ) ) ) )
237	235, 236	syl 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 ) ) ) )
238	219, 237	eqsstrd 3466	. . . . . . . . . . . . . . . 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 ) ) ) )
239	215, 238	eqsstr3d 3467	. . . . . . . . . . . . . . 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 5875	. . . . . . . . . . . . . . . . 17 |- ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
241	240	uniex 6587	. . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
242	241	snss 4096	. . . . . . . . . . . . . . 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 ) ) ) )
243	239, 242	sylibr 216	. . . . . . . . . . . . . 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 ) ) ) )
244	190, 243	eqeltrd 2529	. . . . . . . . . . . . 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 ) ) ) )
245	174, 180, 188, 244	syl21anc 1267	. . . . . . . . . . . 12 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
246	245	adantlr 721	. . . . . . . . . . 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 ) ) ) )
247	173, 246	sseldd 3433	. . . . . . . . . 10 |- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. w )
248	247	ralrimiva 2802	. . . . . . . . 9 |- ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w )
249	248	expl 624	. . . . . . . 8 |- ( ph -> ( ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w ) )
250	249	reximdv 2861	. . . . . . 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 ) )
251	250	ad2antrr 732	. . . . . 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 ) )
252	172, 251	mpd 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 )
253	65, 46, 4, 32, 37, 69, 84, 94	cnextf 21081	. . . . . . . . . 10 |- ( ph -> ( ( JCnExt K ) ` F ) : C --> B )
254		ffun 5731	. . . . . . . . . 10 |- ( ( ( JCnExt K ) ` F ) : C --> B -> Fun ( ( JCnExt K ) ` F ) )
255	253, 254	syl 17	. . . . . . . . 9 |- ( ph -> Fun ( ( JCnExt K ) ` F ) )
256	255	adantr 467	. . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> Fun ( ( JCnExt K ) ` F ) )
257	65	neii1 20122	. . . . . . . . . 10 |- ( ( J e. Top /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
258	4, 257	sylan 474	. . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
259		fdm 5733	. . . . . . . . . . 11 |- ( ( ( JCnExt K ) ` F ) : C --> B -> dom ( ( JCnExt K ) ` F ) = C )
260	253, 259	syl 17	. . . . . . . . . 10 |- ( ph -> dom ( ( JCnExt K ) ` F ) = C )
261	260	adantr 467	. . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> dom ( ( JCnExt K ) ` F ) = C )
262	258, 261	sseqtr4d 3469	. . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( JCnExt K ) ` F ) )
263		funimass4 5916	. . . . . . . 8 |- ( ( Fun ( ( JCnExt K ) ` F ) /\ v C_ dom ( ( JCnExt K ) ` F ) ) -> ( ( ( ( JCnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w ) )
264	256, 262, 263	syl2anc 667	. . . . . . 7 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( ( ( ( JCnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w ) )
265	264	biimprd 227	. . . . . 6 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w -> ( ( ( JCnExt K ) ` F ) " v ) C_ w ) )
266	265	reximdva 2862	. . . . 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 ) )
267	1, 252, 266	sylc 62	. . . 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 )
268	267	ralrimiva 2802	. . 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 )
269	268	ralrimiva 2802	. 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 )
270	65, 46	cnnei 20298	. . 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 ) )
271	4, 34, 253, 270	syl3anc 1268	. 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 ) )
272	269, 271	mpbird 236	1 |- ( ph -> ( ( JCnExt K ) ` F ) e. ( J Cn K ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   =/= wne 2622   A.wral 2737   E.wrex 2738   _Vcvv 3045   i^i cin 3403   C_ wss 3404   (/)c0 3731   {csn 3968   U.cuni 4198   class class class wbr 4402   dom cdm 4834   ran crn 4835   "cima 4837   Fun wfun 5576   -->wf 5578   ` cfv 5582  (class class class)co 6290   1oc1o 7175   ~~ cen 7566   ↾_t crest 15319   fBascfbas 18958   filGencfg 18959   Topctop 19917  TopOnctopon 19918   clsccl 20033   neicnei 20113   Cn ccn 20240   Hauscha 20324   Regcreg 20325   Filcfil 20860   FilMap cfm 20948   fLim cflim 20949   fLimf cflf 20950  CnExtccnext 21074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-1o 7182  df-map 7474  df-pm 7475  df-en 7570  df-rest 15321  df-topgen 15342  df-fbas 18967  df-fg 18968  df-top 19921  df-topon 19923  df-cld 20034  df-ntr 20035  df-cls 20036  df-nei 20114  df-cn 20243  df-cnp 20244  df-haus 20331  df-reg 20332  df-fil 20861  df-fm 20953  df-flim 20954  df-flf 20955  df-cnext 21075

This theorem is referenced by:  cnextucn  21318