Theorem cnextcn 21623

Description: Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology 𝐽 on 𝐶, a subset 𝐴 dense in 𝐶, this states a condition for 𝐹 from 𝐴 to a regular space 𝐾 to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.)

Hypotheses

Ref	Expression
cnextf.1	⊢ 𝐶 = ∪ 𝐽
cnextf.2	⊢ 𝐵 = ∪ 𝐾
cnextf.3	⊢ (𝜑 → 𝐽 ∈ Top)
cnextf.4	⊢ (𝜑 → 𝐾 ∈ Haus)
cnextf.5	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
cnextf.a	⊢ (𝜑 → 𝐴 ⊆ 𝐶)
cnextf.6	⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
cnextf.7	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
cnextcn.8	⊢ (𝜑 → 𝐾 ∈ Reg)

Assertion

Ref	Expression
cnextcn	⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹   𝑥,𝐽   𝑥,𝐾   𝜑,𝑥

Proof of Theorem cnextcn

Dummy variables 𝑦 𝑏 𝑑 𝑢 𝑣 𝑧 𝑤 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 785	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2		simpll 785	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝜑)
3		simpr3 1061	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
4		cnextf.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Top)
5	4	ad2antrr 757	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6		simpr2 1060	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7		neii2 20664	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
8	5, 6, 7	syl2anc 690	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
9		vex 3175	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
10	9	snss 4258	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑣 ↔ {𝑥} ⊆ 𝑣)
11	10	biimpri 216	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑥} ⊆ 𝑣 → 𝑥 ∈ 𝑣)
12	11	anim1i 589	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))
13	12	anim2i 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
14	13	anim2i 590	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
15	14	ex 448	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))))
16		3anass 1034	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)))
17	16	anbi1i 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑))
18		anass 678	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)))
19		anass 678	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
20	19	anbi2i 725	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
21	17, 18, 20	3bitri 284	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
22		opnneip 20675	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
23	4, 22	syl3an1 1350	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
24	23	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25		simpr2 1060	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ⊆ 𝑑 ∧ (𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) → 𝑣 ∈ 𝐽)
26	25	ex 448	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ⊆ 𝑑 → ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝐽))
27	26	imdistanri 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))
28	24, 27	jca 552	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
29	21, 28	sylbir 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
30	15, 29	syl6 34	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
31	30	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
32		cnextf.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ Haus)
33		haustop 20887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Top)
35	34	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → 𝐾 ∈ Top)
36		imassrn 5383	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ ran 𝐹
37		cnextf.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
38		frn 5952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
40	36, 39	syl5ss 3578	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵)
41	40	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵)
42		ssrin 3799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ⊆ 𝑑 → (𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴))
43		imass2 5407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
44	42, 43	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ⊆ 𝑑 → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
45	44	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
46		cnextf.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 = ∪ 𝐾
47	46	clsss 20610	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
48	35, 41, 45, 47	syl3anc 1317	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
49		sstr 3575	. . . . . . . . . . . . . . . . 17 ⊢ ((((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
50	48, 49	sylan 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ⊆ 𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
51	50	an32s 841	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
52	51	ex 448	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (𝑣 ⊆ 𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
53	52	anim2d 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
54	53	anim2d 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
55	31, 54	syld 45	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
56	55	reximdv2 2996	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
57	56	imp 443	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
58	2, 3, 8, 57	syl21anc 1316	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
59	58	3anassrs 1281	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
60		simpr 475	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
61		simp-4l 801	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝜑)
62		simplr 787	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))
63		fvex 6098	. . . . . . . . . . . . . 14 ⊢ ((nei‘𝐽)‘{𝑥}) ∈ V
64	63	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65		cnextf.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = ∪ 𝐽
66	65	toptopon 20490	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
67	4, 66	sylib 206	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶))
68	67	elfvexd 6117	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ V)
69		cnextf.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
70	68, 69	ssexd 4728	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ V)
71		elrest 15857	. . . . . . . . . . . . 13 ⊢ ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
72	64, 70, 71	syl2anc 690	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
73	72	biimpa 499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴))
74		imaeq2 5368	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (𝐹 “ 𝑢) = (𝐹 “ (𝑑 ∩ 𝐴)))
75	74	fveq2d 6092	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
76	75	sseq1d 3594	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
77	76	biimpcd 237	. . . . . . . . . . . 12 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
78	77	reximdv 2998	. . . . . . . . . . 11 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
79	73, 78	syl5 33	. . . . . . . . . 10 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
80	79	imp 443	. . . . . . . . 9 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ∧ (𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
81	60, 61, 62, 80	syl12anc 1315	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
82		simplll 793	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝜑 ∧ 𝑥 ∈ 𝐶))
83		simplr 787	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
84		cnextf.6	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
85		eleq1 2675	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
86	85	anbi2d 735	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶)))
87		sneq 4134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
88	87	fveq2d 6092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
89	88	oveq1d 6542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))
90	89	oveq2d 6543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)))
91	90	fveq1d 6090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹))
92	91	neeq1d 2840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))
93	86, 92	imbi12d 332	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)))
94		cnextf.7	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)
95	93, 94	chvarv 2250	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)
96	65, 46, 4, 32, 37, 69, 84, 95	cnextfvval 21621	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
97		fvex 6098	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
98	97	uniex 6828	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V
99	98	snid 4154	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)}
100	32	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ Haus)
101	84	eleq2d 2672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶))
102	101	biimpar 500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
103	67	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
104	69	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
105		simpr 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶)
106		trnei 21448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
107	103, 104, 105, 106	syl3anc 1317	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)))
108	102, 107	mpbid 220	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))
109	37	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
110	46	hausflf2 21554	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
111	100, 108, 109, 94, 110	syl31anc 1320	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
112		en1b 7887	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
113	111, 112	sylib 206	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)})
114	99, 113	syl5eleqr 2694	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
115	96, 114	eqeltrd 2687	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))
116	46	toptopon 20490	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
117	34, 116	sylib 206	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵))
118	117	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
119		flfnei 21547	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)))
120	118, 108, 109, 119	syl3anc 1317	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)))
121	115, 120	mpbid 220	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏))
122	121	simprd 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
123	122	r19.21bi 2915	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
124	82, 83, 123	syl2anc 690	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
125	34	ad3antrrr 761	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
126		simplr 787	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
127	46	neii1 20662	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏 ⊆ 𝐵)
128	125, 126, 127	syl2anc 690	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ⊆ 𝐵)
129		simpr 475	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
130	46	clsss 20610	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
131		sstr 3575	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
132	130, 131	sylan 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
133	132	3an1rs 1270	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
134	133	ex 448	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹 “ 𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
135	134	reximdv 2998	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
136	125, 128, 129, 135	syl3anc 1317	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
137	136	adantllr 750	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
138	124, 137	mpd 15	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
139	34	ad2antrr 757	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
140		cnextcn.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Reg)
141	140	ad2antrr 757	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
142	141	ad2antrr 757	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝐾 ∈ Reg)
143		simplr 787	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝑐 ∈ 𝐾)
144		simprl 789	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
145		regsep 20890	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
146	142, 143, 144, 145	syl3anc 1317	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
147		sstr 3575	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘𝑏) ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
148	147	expcom 449	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ 𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
149	148	anim2d 586	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ 𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
150	149	reximdv 2998	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ 𝑤 → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
151	150	ad2antll 760	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
152	146, 151	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
153		simpr 475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
154		neii2 20664	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
155		fvex 6098	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
156	155	snss 4258	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
157	156	anbi1i 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
158	157	biimpri 216	. . . . . . . . . . . . . 14 ⊢ (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
159	158	reximi 2993	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
160	154, 159	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
161	139, 153, 160	syl2anc 690	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
162	152, 161	r19.29a 3059	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
163		anass 678	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
164		opnneip 20675	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
165	164	3expib 1259	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
166	165	anim1d 585	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Top → (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
167	163, 166	syl5bir 231	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
168	167	reximdv2 2996	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
169	139, 162, 168	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
170	138, 169	r19.29a 3059	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
171	81, 170	r19.29a 3059	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
172	59, 171	r19.29a 3059	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
173		simplr 787	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
174		simpll 785	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝜑)
175	4	ad2antrr 757	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐽 ∈ Top)
176		simplr 787	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ 𝐽)
177	65	eltopss 20479	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝐶)
178	175, 176, 177	syl2anc 690	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ⊆ 𝐶)
179		simpr 475	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝑣)
180	178, 179	sseldd 3568	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝐶)
181		fvex 6098	. . . . . . . . . . . . . . 15 ⊢ ((nei‘𝐽)‘{𝑧}) ∈ V
182	181	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
183	70	ad2antrr 757	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐴 ∈ V)
184		opnneip 20675	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
185	4, 184	syl3an1 1350	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
186	185	3expa 1256	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
187		elrestr 15858	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
188	182, 183, 186, 187	syl3anc 1317	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
189	65, 46, 4, 32, 37, 69, 84, 94	cnextfvval 21621	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
190	189	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
191	32	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ Haus)
192	84	eleq2d 2672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧 ∈ 𝐶))
193	192	biimpar 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
194	67	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
195	69	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
196		simpr 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶)
197		trnei 21448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
198	194, 195, 196, 197	syl3anc 1317	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴)))
199	193, 198	mpbid 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
200	37	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
201		eleq1 2675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶))
202	201	anbi2d 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑧 ∈ 𝐶)))
203		sneq 4134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧})
204	203	fveq2d 6092	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
205	204	oveq1d 6542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
206	205	oveq2d 6543	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
207	206	fveq1d 6090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹))
208	207	neeq1d 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅))
209	202, 208	imbi12d 332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)))
210	209, 94	chvarv 2250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅)
211	46	hausflf2 21554	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
212	191, 199, 200, 210, 211	syl31anc 1320	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜)
213		en1b 7887	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ≈ 1𝑜 ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
214	212, 213	sylib 206	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
215	214	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)})
216	117	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
217		flfval 21546	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
218	216, 199, 200, 217	syl3anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
219	218	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))))
220		uniexg 6830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐾 ∈ Haus → ∪ 𝐾 ∈ V)
221	32, 220	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∪ 𝐾 ∈ V)
222	221	ad2antrr 757	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ∪ 𝐾 ∈ V)
223	46, 222	syl5eqel 2691	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐵 ∈ V)
224	199	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴))
225		filfbas 21404	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴))
227	37	ad2antrr 757	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → 𝐹:𝐴⟶𝐵)
228		simpr 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
229		fgfil 21431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
230	199, 229	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
231	230	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
232	228, 231	eleqtrrd 2690	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
233		eqid 2609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))
234	233	imaelfm 21507	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
235	223, 226, 227, 232, 234	syl31anc 1320	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)))
236		flimclsi 21534	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
237	235, 236	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
238	219, 237	eqsstrd 3601	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
239	215, 238	eqsstr3d 3602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
240		fvex 6098	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
241	240	uniex 6828	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ V
242	241	snss 4258	. . . . . . . . . . . . . . 15 ⊢ (∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ↔ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
243	239, 242	sylibr 222	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
244	190, 243	eqeltrd 2687	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
245	174, 180, 188, 244	syl21anc 1316	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
246	245	adantlr 746	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
247	173, 246	sseldd 3568	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
248	247	ralrimiva 2948	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
249	248	expl 645	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
250	249	reximdv 2998	. . . . . . 7 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
251	250	ad2antrr 757	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252	172, 251	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
253	65, 46, 4, 32, 37, 69, 84, 94	cnextf 21622	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵)
254		ffun 5947	. . . . . . . . . 10 ⊢ (((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵 → Fun ((𝐽CnExt𝐾)‘𝐹))
255	253, 254	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
256	255	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
257	65	neii1 20662	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
258	4, 257	sylan 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
259		fdm 5950	. . . . . . . . . . 11 ⊢ (((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
260	253, 259	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
261	260	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
262	258, 261	sseqtr4d 3604	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
263		funimass4 6142	. . . . . . . 8 ⊢ ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
264	256, 262, 263	syl2anc 690	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
265	264	biimprd 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
266	265	reximdva 2999	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
267	1, 252, 266	sylc 62	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
268	267	ralrimiva 2948	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
269	268	ralrimiva 2948	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
270	65, 46	cnnei 20838	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
271	4, 34, 253, 270	syl3anc 1317	. 2 ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
272	269, 271	mpbird 245	1 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   ∧ w3a 1030   = wceq 1474   ∈ wcel 1976   ≠ wne 2779  ∀wral 2895  ∃wrex 2896  Vcvv 3172   ∩ cin 3538   ⊆ wss 3539  ∅c0 3873  {csn 4124  ∪ cuni 4366   class class class wbr 4577  dom cdm 5028  ran crn 5029   “ cima 5031  Fun wfun 5784  ⟶wf 5786  ‘cfv 5790  (class class class)co 6527  1_𝑜c1o 7417   ≈ cen 7815   ↾_t crest 15850  fBascfbas 19501  filGencfg 19502  Topctop 20459  TopOnctopon 20460  clsccl 20574  neicnei 20653   Cn ccn 20780  Hauscha 20864  Regcreg 20865  Filcfil 21401   FilMap cfm 21489   fLim cflim 21490   fLimf cflf 21491  CnExtccnext 21615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-1o 7424  df-map 7723  df-pm 7724  df-en 7819  df-rest 15852  df-topgen 15873  df-fbas 19510  df-fg 19511  df-top 20463  df-topon 20465  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-cn 20783  df-cnp 20784  df-haus 20871  df-reg 20872  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-cnext 21616

This theorem is referenced by:  cnextucn  21859