Theorem cnextcn 21871

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 790	. . . . 5 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> ph )
2		simpll 790	. . . . . . . . 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 1069	. . . . . . . . 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 762	. . . . . . . . . 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 1068	. . . . . . . . . 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 20912	. . . . . . . . . 10 |- ( ( J e. Top /\ d e. ( ( nei ` J ) ` { x } ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) )
8	5, 6, 7	syl2anc 693	. . . . . . . . 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 3203	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
10	9	snss 4316	. . . . . . . . . . . . . . . . . . 19 |- ( x e. v <-> { x } C_ v )
11	10	biimpri 218	. . . . . . . . . . . . . . . . . 18 |- ( { x } C_ v -> x e. v )
12	11	anim1i 592	. . . . . . . . . . . . . . . . 17 |- ( ( { x } C_ v /\ v C_ d ) -> ( x e. v /\ v C_ d ) )
13	12	anim2i 593	. . . . . . . . . . . . . . . 16 |- ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
14	13	anim2i 593	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
15	14	ex 450	. . . . . . . . . . . . . 14 |- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) )
16		3anass 1042	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) <-> ( ph /\ ( v e. J /\ x e. v ) ) )
17	16	anbi1i 731	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) )
18		anass 681	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) <-> ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) )
19		anass 681	. . . . . . . . . . . . . . . . 17 |- ( ( ( v e. J /\ x e. v ) /\ v C_ d ) <-> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
20	19	anbi2i 730	. . . . . . . . . . . . . . . 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 286	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
22		opnneip 20923	. . . . . . . . . . . . . . . . . 18 |- ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
23	4, 22	syl3an1 1359	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
24	23	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> v e. ( ( nei ` J ) ` { x } ) )
25		simpr2 1068	. . . . . . . . . . . . . . . . . 18 |- ( ( v C_ d /\ ( ph /\ v e. J /\ x e. v ) ) -> v e. J )
26	25	ex 450	. . . . . . . . . . . . . . . . 17 |- ( v C_ d -> ( ( ph /\ v e. J /\ x e. v ) -> v e. J ) )
27	26	imdistanri 727	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. J /\ v C_ d ) )
28	24, 27	jca 554	. . . . . . . . . . . . . . 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 225	. . . . . . . . . . . . . 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 35	. . . . . . . . . . . . 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 481	. . . . . . . . . . . 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 21135	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. Haus -> K e. Top )
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. Top )
35	34	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> K e. Top )
36		imassrn 5477	. . . . . . . . . . . . . . . . . . . 20 |- ( F " ( d i^i A ) ) C_ ran F
37		cnextf.5	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F : A --> B )
38		frn 6053	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : A --> B -> ran F C_ B )
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran F C_ B )
40	36, 39	syl5ss 3614	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( F " ( d i^i A ) ) C_ B )
41	40	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> ( F " ( d i^i A ) ) C_ B )
42		ssrin 3838	. . . . . . . . . . . . . . . . . . . 20 |- ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) )
43		imass2 5501	. . . . . . . . . . . . . . . . . . . 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 482	. . . . . . . . . . . . . . . . . 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 20858	. . . . . . . . . . . . . . . . . 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 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
49		sstr 3611	. . . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . . 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 846	. . . . . . . . . . . . . . 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 450	. . . . . . . . . . . . . 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 589	. . . . . . . . . . . . 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 589	. . . . . . . . . . . 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 47	. . . . . . . . . . 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 3014	. . . . . . . . . 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 445	. . . . . . . . 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 1325	. . . . . . . 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 1290	. . . . . . 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 477	. . . . . . . . 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 806	. . . . . . . . 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 792	. . . . . . . . 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		fvexd 6203	. . . . . . . . . . . . 13 |- ( ph -> ( ( nei ` J ) ` { x } ) e. _V )
64		cnextf.1	. . . . . . . . . . . . . . . . 17 |- C = U. J
65	64	toptopon 20722	. . . . . . . . . . . . . . . 16 |- ( J e. Top <-> J e. (TopOn ` C ) )
66	4, 65	sylib 208	. . . . . . . . . . . . . . 15 |- ( ph -> J e. (TopOn ` C ) )
67	66	elfvexd 6222	. . . . . . . . . . . . . 14 |- ( ph -> C e. _V )
68		cnextf.a	. . . . . . . . . . . . . 14 |- ( ph -> A C_ C )
69	67, 68	ssexd 4805	. . . . . . . . . . . . 13 |- ( ph -> A e. _V )
70		elrest 16088	. . . . . . . . . . . . 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 ) ) )
71	63, 69, 70	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> ( u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) )
72	71	biimpa 501	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) -> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) )
73		imaeq2 5462	. . . . . . . . . . . . . . 15 |- ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) )
74	73	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
75	74	sseq1d 3632	. . . . . . . . . . . . 13 |- ( u = ( d i^i A ) -> ( ( ( cls ` K ) ` ( F " u ) ) C_ w <-> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
76	75	biimpcd 239	. . . . . . . . . . . 12 |- ( ( ( cls ` K ) ` ( F " u ) ) C_ w -> ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
77	76	reximdv 3016	. . . . . . . . . . 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 ) )
78	72, 77	syl5 34	. . . . . . . . . 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 ) )
79	78	imp 445	. . . . . . . . 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 )
80	60, 61, 62, 79	syl12anc 1324	. . . . . . . 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 )
81		simplll 798	. . . . . . . . . . 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 ) )
82		simplr 792	. . . . . . . . . . 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 ) } ) )
83		cnextf.6	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( cls ` J ) ` A ) = C )
84		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( x e. C <-> y e. C ) )
85	84	anbi2d 740	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
86		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> { x } = { y } )
87	86	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
88	87	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { y } ) ↾t A ) )
89	88	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) )
90	89	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) )
91	90	neeq1d 2853	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) ) )
92	85, 91	imbi12d 334	. . . . . . . . . . . . . . . . 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 ) =/= (/) ) ) )
93		cnextf.7	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) )
94	92, 93	chvarv 2263	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) )
95	64, 46, 4, 32, 37, 68, 83, 94	cnextfvval 21869	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
96		fvex 6201	. . . . . . . . . . . . . . . . . 18 |- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
97	96	uniex 6953	. . . . . . . . . . . . . . . . 17 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
98	97	snid 4208	. . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) }
99	32	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> K e. Haus )
100	83	eleq2d 2687	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
101	100	biimpar 502	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
102	66	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> J e. (TopOn ` C ) )
103	68	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> A C_ C )
104		simpr 477	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> x e. C )
105		trnei 21696	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J e. (TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) ) )
106	102, 103, 104, 105	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) ) )
107	101, 106	mpbid 222	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) )
108	37	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> F : A --> B )
109	46	hausflf2 21802	. . . . . . . . . . . . . . . . . 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 )
110	99, 107, 108, 93, 109	syl31anc 1329	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ~~ 1o )
111		en1b 8024	. . . . . . . . . . . . . . . . 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 ) } )
112	110, 111	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) } )
113	98, 112	syl5eleqr 2708	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
114	95, 113	eqeltrd 2701	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
115	46	toptopon 20722	. . . . . . . . . . . . . . . . 17 |- ( K e. Top <-> K e. (TopOn ` B ) )
116	34, 115	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ph -> K e. (TopOn ` B ) )
117	116	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> K e. (TopOn ` B ) )
118		flfnei 21795	. . . . . . . . . . . . . . 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 ) ) )
119	117, 107, 108, 118	syl3anc 1326	. . . . . . . . . . . . . 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 ) ) )
120	114, 119	mpbid 222	. . . . . . . . . . . . 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 ) )
121	120	simprd 479	. . . . . . . . . . . 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 )
122	121	r19.21bi 2932	. . . . . . . . . . 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 )
123	81, 82, 122	syl2anc 693	. . . . . . . . . 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 )
124	34	ad3antrrr 766	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> K e. Top )
125		simplr 792	. . . . . . . . . . . . 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 ) } ) )
126	46	neii1 20910	. . . . . . . . . . . . 13 |- ( ( K e. Top /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> b C_ B )
127	124, 125, 126	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b C_ B )
128		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
129	46	clsss 20858	. . . . . . . . . . . . . . . 16 |- ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) )
130		sstr 3611	. . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
131	129, 130	sylan 488	. . . . . . . . . . . . . . 15 |- ( ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
132	131	3an1rs 1279	. . . . . . . . . . . . . 14 |- ( ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
133	132	ex 450	. . . . . . . . . . . . 13 |- ( ( K e. Top /\ b C_ B /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( F " u ) C_ b -> ( ( cls ` K ) ` ( F " u ) ) C_ w ) )
134	133	reximdv 3016	. . . . . . . . . . . 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 ) )
135	124, 127, 128, 134	syl3anc 1326	. . . . . . . . . . 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 ) )
136	135	adantllr 755	. . . . . . . . . 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 ) )
137	123, 136	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 )
138	34	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Top )
139		cnextcn.8	. . . . . . . . . . . . . . 15 |- ( ph -> K e. Reg )
140	139	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Reg )
141	140	ad2antrr 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 ) ) -> K e. Reg )
142		simplr 792	. . . . . . . . . . . . 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 )
143		simprl 794	. . . . . . . . . . . . 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 )
144		regsep 21138	. . . . . . . . . . . . 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 ) )
145	141, 142, 143, 144	syl3anc 1326	. . . . . . . . . . . 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 ) )
146		sstr 3611	. . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` b ) C_ c /\ c C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
147	146	expcom 451	. . . . . . . . . . . . . . 15 |- ( c C_ w -> ( ( ( cls ` K ) ` b ) C_ c -> ( ( cls ` K ) ` b ) C_ w ) )
148	147	anim2d 589	. . . . . . . . . . . . . 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 ) ) )
149	148	reximdv 3016	. . . . . . . . . . . . 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 ) ) )
150	149	ad2antll 765	. . . . . . . . . . . 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 ) ) )
151	145, 150	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 ) )
152		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
153		neii2 20912	. . . . . . . . . . . . 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 ) )
154		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( ( ( JCnExt K ) ` F ) ` x ) e. _V
155	154	snss 4316	. . . . . . . . . . . . . . . 16 |- ( ( ( ( JCnExt K ) ` F ) ` x ) e. c <-> { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c )
156	155	anbi1i 731	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) <-> ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) )
157	156	biimpri 218	. . . . . . . . . . . . . 14 |- ( ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
158	157	reximi 3011	. . . . . . . . . . . . 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 ) )
159	153, 158	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 ) )
160	138, 152, 159	syl2anc 693	. . . . . . . . . . 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 ) )
161	151, 160	r19.29a 3078	. . . . . . . . . 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 ) )
162		anass 681	. . . . . . . . . . . 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 ) ) )
163		opnneip 20923	. . . . . . . . . . . . . 14 |- ( ( K e. Top /\ b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
164	163	3expib 1268	. . . . . . . . . . . . 13 |- ( K e. Top -> ( ( b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) )
165	164	anim1d 588	. . . . . . . . . . . 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 ) ) )
166	162, 165	syl5bir 233	. . . . . . . . . . 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 ) ) )
167	166	reximdv2 3014	. . . . . . . . . 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 ) )
168	138, 161, 167	sylc 65	. . . . . . . . 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 )
169	137, 168	r19.29a 3078	. . . . . . . 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 )
170	80, 169	r19.29a 3078	. . . . . . 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 )
171	59, 170	r19.29a 3078	. . . . . 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 ) )
172		simplr 792	. . . . . . . . . . 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 )
173		simpll 790	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph )
174	4	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> J e. Top )
175		simplr 792	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. J )
176	64	eltopss 20712	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ v e. J ) -> v C_ C )
177	174, 175, 176	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v C_ C )
178		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. v )
179	177, 178	sseldd 3604	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C )
180		fvexd 6203	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( nei ` J ) ` { z } ) e. _V )
181	69	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> A e. _V )
182		opnneip 20923	. . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
183	4, 182	syl3an1 1359	. . . . . . . . . . . . . . 15 |- ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
184	183	3expa 1265	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
185		elrestr 16089	. . . . . . . . . . . . . 14 |- ( ( ( ( nei ` J ) ` { z } ) e. _V /\ A e. _V /\ v e. ( ( nei ` J ) ` { z } ) ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) )
186	180, 181, 184, 185	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) )
187	64, 46, 4, 32, 37, 68, 83, 93	cnextfvval 21869	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. C ) -> ( ( ( JCnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
188	187	adantr 481	. . . . . . . . . . . . . 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 ) )
189	32	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. Haus )
190	83	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( z e. ( ( cls ` J ) ` A ) <-> z e. C ) )
191	190	biimpar 502	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> z e. ( ( cls ` J ) ` A ) )
192	66	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> J e. (TopOn ` C ) )
193	68	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> A C_ C )
194		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> z e. C )
195		trnei 21696	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( J e. (TopOn ` C ) /\ A C_ C /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) ) )
196	192, 193, 194, 195	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) ) )
197	191, 196	mpbid 222	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) )
198	37	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> F : A --> B )
199		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x e. C <-> z e. C ) )
200	199	anbi2d 740	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) )
201		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = z -> { x } = { z } )
202	201	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
203	202	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = z -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
204	203	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) )
205	204	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
206	205	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) ) )
207	200, 206	imbi12d 334	. . . . . . . . . . . . . . . . . . . 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 ) =/= (/) ) ) )
208	207, 93	chvarv 2263	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) )
209	46	hausflf2 21802	. . . . . . . . . . . . . . . . . . 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 )
210	189, 197, 198, 208, 209	syl31anc 1329	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) ~~ 1o )
211		en1b 8024	. . . . . . . . . . . . . . . . . 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 ) } )
212	210, 211	sylib 208	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) = { U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) } )
213	212	adantr 481	. . . . . . . . . . . . . . . 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 ) } )
214	116	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. (TopOn ` B ) )
215		flfval 21794	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
216	214, 197, 198, 215	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) = ( K fLim ( ( B FilMap F ) ` ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ) )
217	216	adantr 481	. . . . . . . . . . . . . . . . 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 ) ) ) )
218		uniexg 6955	. . . . . . . . . . . . . . . . . . . . . 22 |- ( K e. Haus -> U. K e. _V )
219	32, 218	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U. K e. _V )
220	219	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> U. K e. _V )
221	46, 220	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> B e. _V )
222	197	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) )
223		filfbas 21652	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( fBas ` A ) )
224	222, 223	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 ) )
225	37	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> F : A --> B )
226		simpr 477	. . . . . . . . . . . . . . . . . . . 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 ) )
227		fgfil 21679	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
228	197, 227	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
229	228	adantr 481	. . . . . . . . . . . . . . . . . . . 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 ) )
230	226, 229	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . 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 ) ) )
231		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) )
232	231	imaelfm 21755	. . . . . . . . . . . . . . . . . . 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 ) ) )
233	221, 224, 225, 230, 232	syl31anc 1329	. . . . . . . . . . . . . . . . . 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 ) ) )
234		flimclsi 21782	. . . . . . . . . . . . . . . . . 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 ) ) ) )
235	233, 234	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 ) ) ) )
236	217, 235	eqsstrd 3639	. . . . . . . . . . . . . . . 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 ) ) ) )
237	213, 236	eqsstr3d 3640	. . . . . . . . . . . . . . 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 ) ) ) )
238		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
239	238	uniex 6953	. . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
240	239	snss 4316	. . . . . . . . . . . . . . 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 ) ) ) )
241	237, 240	sylibr 224	. . . . . . . . . . . . . 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 ) ) ) )
242	188, 241	eqeltrd 2701	. . . . . . . . . . . . 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 ) ) ) )
243	173, 179, 186, 242	syl21anc 1325	. . . . . . . . . . . 12 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
244	243	adantlr 751	. . . . . . . . . . 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 ) ) ) )
245	172, 244	sseldd 3604	. . . . . . . . . 10 |- ( ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. w )
246	245	ralrimiva 2966	. . . . . . . . 9 |- ( ( ( ph /\ v e. J ) /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w )
247	246	expl 648	. . . . . . . 8 |- ( ph -> ( ( v e. J /\ ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ w ) -> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w ) )
248	247	reximdv 3016	. . . . . . 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 ) )
249	248	ad2antrr 762	. . . . . 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 ) )
250	171, 249	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 )
251	64, 46, 4, 32, 37, 68, 83, 93	cnextf 21870	. . . . . . . . . 10 |- ( ph -> ( ( JCnExt K ) ` F ) : C --> B )
252		ffun 6048	. . . . . . . . . 10 |- ( ( ( JCnExt K ) ` F ) : C --> B -> Fun ( ( JCnExt K ) ` F ) )
253	251, 252	syl 17	. . . . . . . . 9 |- ( ph -> Fun ( ( JCnExt K ) ` F ) )
254	253	adantr 481	. . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> Fun ( ( JCnExt K ) ` F ) )
255	64	neii1 20910	. . . . . . . . . 10 |- ( ( J e. Top /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
256	4, 255	sylan 488	. . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
257		fdm 6051	. . . . . . . . . . 11 |- ( ( ( JCnExt K ) ` F ) : C --> B -> dom ( ( JCnExt K ) ` F ) = C )
258	251, 257	syl 17	. . . . . . . . . 10 |- ( ph -> dom ( ( JCnExt K ) ` F ) = C )
259	258	adantr 481	. . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> dom ( ( JCnExt K ) ` F ) = C )
260	256, 259	sseqtr4d 3642	. . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( JCnExt K ) ` F ) )
261		funimass4 6247	. . . . . . . 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 ) )
262	254, 260, 261	syl2anc 693	. . . . . . 7 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( ( ( ( JCnExt K ) ` F ) " v ) C_ w <-> A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w ) )
263	262	biimprd 238	. . . . . 6 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> ( A. z e. v ( ( ( JCnExt K ) ` F ) ` z ) e. w -> ( ( ( JCnExt K ) ` F ) " v ) C_ w ) )
264	263	reximdva 3017	. . . . 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 ) )
265	1, 250, 264	sylc 65	. . . 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 )
266	265	ralrimiva 2966	. . 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 )
267	266	ralrimiva 2966	. 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 )
268	64, 46	cnnei 21086	. . 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 ) )
269	4, 34, 251, 268	syl3anc 1326	. 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 ) )
270	267, 269	mpbird 247	1 |- ( ph -> ( ( JCnExt K ) ` F ) e. ( J Cn K ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   U.cuni 4436   class class class wbr 4653   dom cdm 5114   ran crn 5115   "cima 5117   Fun wfun 5882   -->wf 5884   ` cfv 5888  (class class class)co 6650   1oc1o 7553   ~~ cen 7952   ↾_t crest 16081   fBascfbas 19734   filGencfg 19735   Topctop 20698  TopOnctopon 20715   clsccl 20822   neicnei 20901   Cn ccn 21028   Hauscha 21112   Regcreg 21113   Filcfil 21649   FilMap cfm 21737   fLim cflim 21738   fLimf cflf 21739  CnExtccnext 21863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-1o 7560  df-map 7859  df-pm 7860  df-en 7956  df-rest 16083  df-topgen 16104  df-fbas 19743  df-fg 19744  df-top 20699  df-topon 20716  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-cn 21031  df-cnp 21032  df-haus 21119  df-reg 21120  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-cnext 21864

This theorem is referenced by:  cnextucn  22107