Theorem cnextcn 20545

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 753	. . . . 5 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> ph )
2		simpll 753	. . . . . . . . 9 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ph )
3		simpr3 1005	. . . . . . . . 9 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w )
4		cnextf.3	. . . . . . . . . . 11 |- ( ph -> J e. Top )
5	4	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> J e. Top )
6		simpr2 1004	. . . . . . . . . 10 |- ( ( ( ph /\ x e. C ) /\ ( w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ d e. ( ( nei ` J ) ` { x } ) /\ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) ) -> d e. ( ( nei ` J ) ` { x } ) )
7		neii2 19587	. . . . . . . . . 10 |- ( ( J e. Top /\ d e. ( ( nei ` J ) ` { x } ) ) -> E. v e. J ( { x } C_ v /\ v C_ d ) )
8	5, 6, 7	syl2anc 661	. . . . . . . . 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 3098	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
10	9	snss 4139	. . . . . . . . . . . . . . . . . . 19 |- ( x e. v <-> { x } C_ v )
11	10	biimpri 206	. . . . . . . . . . . . . . . . . 18 |- ( { x } C_ v -> x e. v )
12	11	anim1i 568	. . . . . . . . . . . . . . . . 17 |- ( ( { x } C_ v /\ v C_ d ) -> ( x e. v /\ v C_ d ) )
13	12	anim2i 569	. . . . . . . . . . . . . . . 16 |- ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
14	13	anim2i 569	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
15	14	ex 434	. . . . . . . . . . . . . 14 |- ( ph -> ( ( v e. J /\ ( { x } C_ v /\ v C_ d ) ) -> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) ) )
16		3anass 978	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) <-> ( ph /\ ( v e. J /\ x e. v ) ) )
17	16	anbi1i 695	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) )
18		anass 649	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( v e. J /\ x e. v ) ) /\ v C_ d ) <-> ( ph /\ ( ( v e. J /\ x e. v ) /\ v C_ d ) ) )
19		anass 649	. . . . . . . . . . . . . . . . 17 |- ( ( ( v e. J /\ x e. v ) /\ v C_ d ) <-> ( v e. J /\ ( x e. v /\ v C_ d ) ) )
20	19	anbi2i 694	. . . . . . . . . . . . . . . 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 271	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) <-> ( ph /\ ( v e. J /\ ( x e. v /\ v C_ d ) ) ) )
22		opnneip 19598	. . . . . . . . . . . . . . . . . 18 |- ( ( J e. Top /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
23	4, 22	syl3an1 1262	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v e. J /\ x e. v ) -> v e. ( ( nei ` J ) ` { x } ) )
24	23	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> v e. ( ( nei ` J ) ` { x } ) )
25		simpr2 1004	. . . . . . . . . . . . . . . . . 18 |- ( ( v C_ d /\ ( ph /\ v e. J /\ x e. v ) ) -> v e. J )
26	25	ex 434	. . . . . . . . . . . . . . . . 17 |- ( v C_ d -> ( ( ph /\ v e. J /\ x e. v ) -> v e. J ) )
27	26	imdistanri 691	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. J /\ x e. v ) /\ v C_ d ) -> ( v e. J /\ v C_ d ) )
28	24, 27	jca 532	. . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . 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 33	. . . . . . . . . . . . 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 465	. . . . . . . . . . . 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 19810	. . . . . . . . . . . . . . . . . . . 20 |- ( K e. Haus -> K e. Top )
34	32, 33	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. Top )
35	34	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> K e. Top )
36		imassrn 5338	. . . . . . . . . . . . . . . . . . . 20 |- ( F " ( d i^i A ) ) C_ ran F
37		cnextf.5	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> F : A --> B )
38		frn 5727	. . . . . . . . . . . . . . . . . . . . 21 |- ( F : A --> B -> ran F C_ B )
39	37, 38	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran F C_ B )
40	36, 39	syl5ss 3500	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( F " ( d i^i A ) ) C_ B )
41	40	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ v C_ d ) -> ( F " ( d i^i A ) ) C_ B )
42		ssrin 3708	. . . . . . . . . . . . . . . . . . . 20 |- ( v C_ d -> ( v i^i A ) C_ ( d i^i A ) )
43		imass2 5362	. . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . 19 |- ( v C_ d -> ( F " ( v i^i A ) ) C_ ( F " ( d i^i A ) ) )
45	44	adantl 466	. . . . . . . . . . . . . . . . . 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 19533	. . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ v C_ d ) -> ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) C_ ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
49		sstr 3497	. . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . 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 804	. . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . 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 565	. . . . . . . . . . . . 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 565	. . . . . . . . . . . 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 44	. . . . . . . . . . 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 2914	. . . . . . . . . 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 429	. . . . . . . . 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 1228	. . . . . . . 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 1219	. . . . . . 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 461	. . . . . . . . 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 767	. . . . . . . . 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 755	. . . . . . . . 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 5866	. . . . . . . . . . . . . 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 19412	. . . . . . . . . . . . . . . 16 |- ( J e. Top <-> J e. (TopOn ` C ) )
67	4, 66	sylib 196	. . . . . . . . . . . . . . 15 |- ( ph -> J e. (TopOn ` C ) )
68	67	elfvexd 5884	. . . . . . . . . . . . . 14 |- ( ph -> C e. _V )
69		cnextf.a	. . . . . . . . . . . . . 14 |- ( ph -> A C_ C )
70	68, 69	ssexd 4584	. . . . . . . . . . . . 13 |- ( ph -> A e. _V )
71		elrest 14807	. . . . . . . . . . . . 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 661	. . . . . . . . . . . 12 |- ( ph -> ( u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) <-> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) ) )
73	72	biimpa 484	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ) -> E. d e. ( ( nei ` J ) ` { x } ) u = ( d i^i A ) )
74		imaeq2 5323	. . . . . . . . . . . . . . 15 |- ( u = ( d i^i A ) -> ( F " u ) = ( F " ( d i^i A ) ) )
75	74	fveq2d 5860	. . . . . . . . . . . . . 14 |- ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " u ) ) = ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) )
76	75	sseq1d 3516	. . . . . . . . . . . . 13 |- ( u = ( d i^i A ) -> ( ( ( cls ` K ) ` ( F " u ) ) C_ w <-> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
77	76	biimpcd 224	. . . . . . . . . . . 12 |- ( ( ( cls ` K ) ` ( F " u ) ) C_ w -> ( u = ( d i^i A ) -> ( ( cls ` K ) ` ( F " ( d i^i A ) ) ) C_ w ) )
78	77	reximdv 2917	. . . . . . . . . . 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 32	. . . . . . . . . 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 429	. . . . . . . . 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 1227	. . . . . . . 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 759	. . . . . . . . . . 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 755	. . . . . . . . . . 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 2515	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( x e. C <-> y e. C ) )
86	85	anbi2d 703	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ph /\ x e. C ) <-> ( ph /\ y e. C ) ) )
87		sneq 4024	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> { x } = { y } )
88	87	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { y } ) )
89	88	oveq1d 6296	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { y } ) ↾t A ) )
90	89	oveq2d 6297	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) )
91	90	fveq1d 5858	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) )
92	91	neeq1d 2720	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) ) )
93	86, 92	imbi12d 320	. . . . . . . . . . . . . . . . 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 2000	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { y } ) ↾t A ) ) ` F ) =/= (/) )
96	65, 46, 4, 32, 37, 69, 84, 95	cnextfvval 20543	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
97		fvex 5866	. . . . . . . . . . . . . . . . . 18 |- ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
98	97	uniex 6581	. . . . . . . . . . . . . . . . 17 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. _V
99	98	snid 4042	. . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) e. { U. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) }
100	32	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> K e. Haus )
101	84	eleq2d 2513	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
102	101	biimpar 485	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
103	67	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> J e. (TopOn ` C ) )
104	69	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> A C_ C )
105		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. C ) -> x e. C )
106		trnei 20371	. . . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) ) )
108	102, 107	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) ↾t A ) e. ( Fil ` A ) )
109	37	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. C ) -> F : A --> B )
110	46	hausflf2 20477	. . . . . . . . . . . . . . . . . 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 1232	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ~~ 1o )
112		en1b 7585	. . . . . . . . . . . . . . . . 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 196	. . . . . . . . . . . . . . . 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 2538	. . . . . . . . . . . . . . 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 2531	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. C ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) )
116	46	toptopon 19412	. . . . . . . . . . . . . . . . 17 |- ( K e. Top <-> K e. (TopOn ` B ) )
117	34, 116	sylib 196	. . . . . . . . . . . . . . . 16 |- ( ph -> K e. (TopOn ` B ) )
118	117	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. C ) -> K e. (TopOn ` B ) )
119		flfnei 20470	. . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . 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 210	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. C ) -> ( ( ( ( JCnExt K ) ` F ) ` x ) e. B /\ A. b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) E. u e. ( ( ( nei ` J ) ` { x } ) ↾t A ) ( F " u ) C_ b ) )
122	121	simprd 463	. . . . . . . . . . . 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 2812	. . . . . . . . . . 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 661	. . . . . . . . . 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 729	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> K e. Top )
126		simplr 755	. . . . . . . . . . . . 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 19585	. . . . . . . . . . . . 13 |- ( ( K e. Top /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> b C_ B )
128	125, 126, 127	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. C ) /\ b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ ( ( cls ` K ) ` b ) C_ w ) -> b C_ B )
129		simpr 461	. . . . . . . . . . . 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 19533	. . . . . . . . . . . . . . . 16 |- ( ( K e. Top /\ b C_ B /\ ( F " u ) C_ b ) -> ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) )
131		sstr 3497	. . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` ( F " u ) ) C_ ( ( cls ` K ) ` b ) /\ ( ( cls ` K ) ` b ) C_ w ) -> ( ( cls ` K ) ` ( F " u ) ) C_ w )
132	130, 131	sylan 471	. . . . . . . . . . . . . . 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 1209	. . . . . . . . . . . . . 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 434	. . . . . . . . . . . . 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 2917	. . . . . . . . . . . 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 1229	. . . . . . . . . . 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 718	. . . . . . . . . 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 725	. . . . . . . . . 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 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> K e. Reg )
142	141	ad2antrr 725	. . . . . . . . . . . . 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 755	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> c e. K )
144		simprl 756	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) /\ c e. K ) /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) ) -> ( ( ( JCnExt K ) ` F ) ` x ) e. c )
145		regsep 19813	. . . . . . . . . . . . 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 1229	. . . . . . . . . . . 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 3497	. . . . . . . . . . . . . . . 16 |- ( ( ( ( cls ` K ) ` b ) C_ c /\ c C_ w ) -> ( ( cls ` K ) ` b ) C_ w )
148	147	expcom 435	. . . . . . . . . . . . . . 15 |- ( c C_ w -> ( ( ( cls ` K ) ` b ) C_ c -> ( ( cls ` K ) ` b ) C_ w ) )
149	148	anim2d 565	. . . . . . . . . . . . . 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 2917	. . . . . . . . . . . . 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 728	. . . . . . . . . . . 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 461	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. C ) /\ w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) -> w e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
154		neii2 19587	. . . . . . . . . . . . 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 5866	. . . . . . . . . . . . . . . . 17 |- ( ( ( JCnExt K ) ` F ) ` x ) e. _V
156	155	snss 4139	. . . . . . . . . . . . . . . 16 |- ( ( ( ( JCnExt K ) ` F ) ` x ) e. c <-> { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c )
157	156	anbi1i 695	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) <-> ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) )
158	157	biimpri 206	. . . . . . . . . . . . . 14 |- ( ( { ( ( ( JCnExt K ) ` F ) ` x ) } C_ c /\ c C_ w ) -> ( ( ( ( JCnExt K ) ` F ) ` x ) e. c /\ c C_ w ) )
159	158	reximi 2911	. . . . . . . . . . . . 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 16	. . . . . . . . . . . 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 661	. . . . . . . . . . 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 2985	. . . . . . . . . 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 649	. . . . . . . . . . . 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 19598	. . . . . . . . . . . . . 14 |- ( ( K e. Top /\ b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) )
165	164	3expib 1200	. . . . . . . . . . . . 13 |- ( K e. Top -> ( ( b e. K /\ ( ( ( JCnExt K ) ` F ) ` x ) e. b ) -> b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) ) )
166	165	anim1d 564	. . . . . . . . . . . 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 218	. . . . . . . . . . 11 |- ( K e. Top -> ( ( b e. K /\ ( ( ( ( JCnExt K ) ` F ) ` x ) e. b /\ ( ( cls ` K ) ` b ) C_ w ) ) -> ( b e. ( ( nei ` K ) ` { ( ( ( JCnExt K ) ` F ) ` x ) } ) /\ ( ( cls ` K ) ` b ) C_ w ) ) )
168	167	reximdv2 2914	. . . . . . . . . 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 60	. . . . . . . . 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 2985	. . . . . . . 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 2985	. . . . . . 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 2985	. . . . . 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 755	. . . . . . . . . . 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 753	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ph )
175	4	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> J e. Top )
176		simplr 755	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. J )
177	65	eltopss 19394	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ v e. J ) -> v C_ C )
178	175, 176, 177	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v C_ C )
179		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. v )
180	178, 179	sseldd 3490	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> z e. C )
181		fvex 5866	. . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> A e. _V )
184		opnneip 19598	. . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
185	4, 184	syl3an1 1262	. . . . . . . . . . . . . . 15 |- ( ( ph /\ v e. J /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
186	185	3expa 1197	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> v e. ( ( nei ` J ) ` { z } ) )
187		elrestr 14808	. . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . 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 20543	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. C ) -> ( ( ( JCnExt K ) ` F ) ` z ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
190	189	adantr 465	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. Haus )
192	84	eleq2d 2513	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( z e. ( ( cls ` J ) ` A ) <-> z e. C ) )
193	192	biimpar 485	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> z e. ( ( cls ` J ) ` A ) )
194	67	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> J e. (TopOn ` C ) )
195	69	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> A C_ C )
196		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> z e. C )
197		trnei 20371	. . . . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. C ) -> ( z e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) ) )
199	193, 198	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) )
200	37	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> F : A --> B )
201		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x e. C <-> z e. C ) )
202	201	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ph /\ x e. C ) <-> ( ph /\ z e. C ) ) )
203		sneq 4024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = z -> { x } = { z } )
204	203	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
205	204	oveq1d 6296	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = z -> ( ( ( nei ` J ) ` { x } ) ↾t A ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
206	205	oveq2d 6297	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = z -> ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) = ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) )
207	206	fveq1d 5858	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) )
208	207	neeq1d 2720	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) <-> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) ) )
209	202, 208	imbi12d 320	. . . . . . . . . . . . . . . . . . . 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 2000	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) =/= (/) )
211	46	hausflf2 20477	. . . . . . . . . . . . . . . . . . 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 1232	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) ~~ 1o )
213		en1b 7585	. . . . . . . . . . . . . . . . . 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 196	. . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. C ) -> K e. (TopOn ` B ) )
217		flfval 20469	. . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 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 6582	. . . . . . . . . . . . . . . . . . . . . 22 |- ( K e. Haus -> U. K e. _V )
221	32, 220	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U. K e. _V )
222	221	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> U. K e. _V )
223	46, 222	syl5eqel 2535	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> B e. _V )
224	199	adantr 465	. . . . . . . . . . . . . . . . . . . 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 20327	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( Fil ` A ) -> ( ( ( nei ` J ) ` { z } ) ↾t A ) e. ( fBas ` A ) )
226	224, 225	syl 16	. . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> F : A --> B )
228		simpr 461	. . . . . . . . . . . . . . . . . . . 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 20354	. . . . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. C ) -> ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( ( ( nei ` J ) ` { z } ) ↾t A ) )
231	230	adantr 465	. . . . . . . . . . . . . . . . . . . 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 2534	. . . . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . . . . 20 |- ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) ) = ( A filGen ( ( ( nei ` J ) ` { z } ) ↾t A ) )
234	233	imaelfm 20430	. . . . . . . . . . . . . . . . . . 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 1232	. . . . . . . . . . . . . . . . . 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 20457	. . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . 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 3523	. . . . . . . . . . . . . . . 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 3524	. . . . . . . . . . . . . . 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 5866	. . . . . . . . . . . . . . . . 17 |- ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
241	240	uniex 6581	. . . . . . . . . . . . . . . 16 |- U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. _V
242	241	snss 4139	. . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z e. C ) /\ ( v i^i A ) e. ( ( ( nei ` J ) ` { z } ) ↾t A ) ) -> U. ( ( K fLimf ( ( ( nei ` J ) ` { z } ) ↾t A ) ) ` F ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
244	190, 243	eqeltrd 2531	. . . . . . . . . . . . 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 1228	. . . . . . . . . . . 12 |- ( ( ( ph /\ v e. J ) /\ z e. v ) -> ( ( ( JCnExt K ) ` F ) ` z ) e. ( ( cls ` K ) ` ( F " ( v i^i A ) ) ) )
246	245	adantlr 714	. . . . . . . . . . 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 3490	. . . . . . . . . 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 2857	. . . . . . . . 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 618	. . . . . . . 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 2917	. . . . . . 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 725	. . . . . 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 20544	. . . . . . . . . 10 |- ( ph -> ( ( JCnExt K ) ` F ) : C --> B )
254		ffun 5723	. . . . . . . . . 10 |- ( ( ( JCnExt K ) ` F ) : C --> B -> Fun ( ( JCnExt K ) ` F ) )
255	253, 254	syl 16	. . . . . . . . 9 |- ( ph -> Fun ( ( JCnExt K ) ` F ) )
256	255	adantr 465	. . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> Fun ( ( JCnExt K ) ` F ) )
257	65	neii1 19585	. . . . . . . . . 10 |- ( ( J e. Top /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
258	4, 257	sylan 471	. . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ C )
259		fdm 5725	. . . . . . . . . . 11 |- ( ( ( JCnExt K ) ` F ) : C --> B -> dom ( ( JCnExt K ) ` F ) = C )
260	253, 259	syl 16	. . . . . . . . . 10 |- ( ph -> dom ( ( JCnExt K ) ` F ) = C )
261	260	adantr 465	. . . . . . . . 9 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> dom ( ( JCnExt K ) ` F ) = C )
262	258, 261	sseqtr4d 3526	. . . . . . . 8 |- ( ( ph /\ v e. ( ( nei ` J ) ` { x } ) ) -> v C_ dom ( ( JCnExt K ) ` F ) )
263		funimass4 5909	. . . . . . . 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 661	. . . . . . 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 223	. . . . . 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 2918	. . . . 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 60	. . . 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 2857	. . 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 2857	. 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 19761	. . 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 1229	. 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 232	1 |- ( ph -> ( ( JCnExt K ) ` F ) e. ( J Cn K ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 974   = wceq 1383   e. wcel 1804   =/= wne 2638   A.wral 2793   E.wrex 2794   _Vcvv 3095   i^i cin 3460   C_ wss 3461   (/)c0 3770   {csn 4014   U.cuni 4234   class class class wbr 4437   dom cdm 4989   ran crn 4990   "cima 4992   Fun wfun 5572   -->wf 5574   ` cfv 5578  (class class class)co 6281   1oc1o 7125   ~~ cen 7515   ↾_t crest 14800   fBascfbas 18385   filGencfg 18386   Topctop 19372  TopOnctopon 19373   clsccl 19497   neicnei 19576   Cn ccn 19703   Hauscha 19787   Regcreg 19788   Filcfil 20324   FilMap cfm 20412   fLim cflim 20413   fLimf cflf 20414  CnExtccnext 20537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-1st 6785  df-2nd 6786  df-1o 7132  df-map 7424  df-pm 7425  df-en 7519  df-rest 14802  df-topgen 14823  df-fbas 18395  df-fg 18396  df-top 19377  df-topon 19380  df-cld 19498  df-ntr 19499  df-cls 19500  df-nei 19577  df-cn 19706  df-cnp 19707  df-haus 19794  df-reg 19795  df-fil 20325  df-fm 20417  df-flim 20418  df-flf 20419  df-cnext 20538

This theorem is referenced by:  cnextucn  20784