cnextcn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnextcn		Structured version Visualization version GIF version

Theorem cnextcn 23791

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 763	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2		simpll 763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝜑)
3		simpr3 1194	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
4		cnextf.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Top)
5	4	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6		simpr2 1193	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7		neii2 22832	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
8	5, 6, 7	syl2anc 582	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
9		vex 3476	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
10	9	snss 4788	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑣 ↔ {𝑥} ⊆ 𝑣)
11	10	biimpri 227	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑥} ⊆ 𝑣 → 𝑥 ∈ 𝑣)
12	11	anim1i 613	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))
13	12	anim2i 615	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
14	13	anim2i 615	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
15	14	ex 411	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))))
16		3anass 1093	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)))
17	16	anbi1i 622	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑))
18		anass 467	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)))
19		anass 467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
20	19	anbi2i 621	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
21	17, 18, 20	3bitri 296	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
22		opnneip 22843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
23	4, 22	syl3an1 1161	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
24	23	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25		simpr2 1193	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ⊆ 𝑑 ∧ (𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) → 𝑣 ∈ 𝐽)
26	25	ex 411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ⊆ 𝑑 → ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝐽))
27	26	imdistanri 568	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))
28	24, 27	jca 510	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
29	21, 28	sylbir 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
30	15, 29	syl6 35	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
31	30	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
32		cnextf.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Haus)
33		haustop 23055	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Top)
35		imassrn 6069	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ ran 𝐹
36		cnextf.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
37	36	frnd 6724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
38	35, 37	sstrid 3992	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵)
39		ssrin 4232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ⊆ 𝑑 → (𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴))
40		imass2 6100	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ⊆ 𝑑 → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
42		cnextf.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 = ∪ 𝐾
43	42	clsss 22778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
44	34, 38, 41, 43	syl2an3an 1420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
45		sstr 3989	. . . . . . . . . . . . . . . . 17 ⊢ ((((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
46	44, 45	sylan 578	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ⊆ 𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
47	46	an32s 648	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
48	47	ex 411	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (𝑣 ⊆ 𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
49	48	anim2d 610	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
50	49	anim2d 610	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
51	31, 50	syld 47	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
52	51	reximdv2 3162	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
53	52	imp 405	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
54	2, 3, 8, 53	syl21anc 834	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
55	54	3anassrs 1358	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
56		simpr 483	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
57		simp-4l 779	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝜑)
58		simplr 765	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))
59		imaeq2 6054	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (𝐹 “ 𝑢) = (𝐹 “ (𝑑 ∩ 𝐴)))
60	59	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
61	60	sseq1d 4012	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
62	61	biimpcd 248	. . . . . . . . . . 11 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
63	62	reximdv 3168	. . . . . . . . . 10 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
64		fvexd 6905	. . . . . . . . . . . 12 ⊢ (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65		cnextf.1	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = ∪ 𝐽
66	65	toptopon 22639	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
67	4, 66	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶))
68	67	elfvexd 6929	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ V)
69		cnextf.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
70	68, 69	ssexd 5323	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ V)
71		elrest 17377	. . . . . . . . . . . 12 ⊢ ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
72	64, 70, 71	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
73	72	biimpa 475	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴))
74	63, 73	impel 504	. . . . . . . . 9 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ∧ (𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
75	56, 57, 58, 74	syl12anc 833	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
76		cnextf.6	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
77		eleq1w 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
78	77	anbi2d 627	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶)))
79		sneq 4637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
80	79	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
81	80	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))
82	81	oveq2d 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴)))
83	82	fveq1d 6892	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹))
84	83	neeq1d 2998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅))
85	78, 84	imbi12d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅)))
86		cnextf.7	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅)
87	85, 86	chvarvv 2000	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅)
88	65, 42, 4, 32, 36, 69, 76, 87	cnextfvval 23789	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
89		fvex 6903	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ V
90	89	uniex 7733	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ V
91	90	snid 4663	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)}
92	32	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ Haus)
93	76	eleq2d 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶))
94	93	biimpar 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
95	67	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
96	69	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
97		simpr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶)
98		trnei 23616	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
99	95, 96, 97, 98	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
100	94, 99	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴))
101	36	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
102	42	hausflf2 23722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
103	92, 100, 101, 86, 102	syl31anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
104		en1b 9025	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)})
105	103, 104	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)})
106	91, 105	eleqtrrid 2838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
107	88, 106	eqeltrd 2831	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
108	42	toptopon 22639	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
109	34, 108	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵))
110	109	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
111		flfnei 23715	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)))
112	110, 100, 101, 111	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)))
113	107, 112	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏))
114	113	simprd 494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
115	114	r19.21bi 3246	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
116	115	ad4ant13 747	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
117	34	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
118		simplr 765	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
119	42	neii1 22830	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏 ⊆ 𝐵)
120	117, 118, 119	syl2anc 582	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ⊆ 𝐵)
121		simpr 483	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
122	42	clsss 22778	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
123		sstr 3989	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
124	122, 123	sylan 578	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
125	124	3an1rs 1357	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
126	125	ex 411	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹 “ 𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
127	126	reximdv 3168	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
128	117, 120, 121, 127	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
129	128	adantllr 715	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
130	116, 129	mpd 15	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
131	34	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
132		cnextcn.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Reg)
133	132	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
134	133	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝐾 ∈ Reg)
135		simplr 765	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝑐 ∈ 𝐾)
136		simprl 767	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
137		regsep 23058	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
138	134, 135, 136, 137	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
139		sstr 3989	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘𝑏) ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
140	139	expcom 412	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ 𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
141	140	anim2d 610	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ 𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
142	141	reximdv 3168	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ 𝑤 → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
143	142	ad2antll 725	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
144	138, 143	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
145		simpr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
146		neii2 22832	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
147		fvex 6903	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
148	147	snss 4788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
149	148	anbi1i 622	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
150	149	biimpri 227	. . . . . . . . . . . . . 14 ⊢ (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
151	150	reximi 3082	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
152	146, 151	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
153	131, 145, 152	syl2anc 582	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
154	144, 153	r19.29a 3160	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
155		anass 467	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
156		opnneip 22843	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
157	156	3expib 1120	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
158	157	anim1d 609	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Top → (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
159	155, 158	biimtrrid 242	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
160	159	reximdv2 3162	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
161	131, 154, 160	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
162	130, 161	r19.29a 3160	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
163	75, 162	r19.29a 3160	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
164	55, 163	r19.29a 3160	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
165		simplr 765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
166		simpll 763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝜑)
167	4	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐽 ∈ Top)
168		simplr 765	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ 𝐽)
169	65	eltopss 22629	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝐶)
170	167, 168, 169	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ⊆ 𝐶)
171		simpr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝑣)
172	170, 171	sseldd 3982	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝐶)
173		fvexd 6905	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
174	70	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐴 ∈ V)
175		opnneip 22843	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
176	4, 175	syl3an1 1161	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
177	176	3expa 1116	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
178		elrestr 17378	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
179	173, 174, 177, 178	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
180	65, 42, 4, 32, 36, 69, 76, 86	cnextfvval 23789	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
181	180	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
182	32	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ Haus)
183	76	eleq2d 2817	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧 ∈ 𝐶))
184	183	biimpar 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
185	67	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
186	69	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
187		simpr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶)
188		trnei 23616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
189	185, 186, 187, 188	syl3anc 1369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
190	184, 189	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴))
191	36	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
192		eleq1w 2814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶))
193	192	anbi2d 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑧 ∈ 𝐶)))
194		sneq 4637	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧})
195	194	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
196	195	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
197	196	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
198	197	fveq1d 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
199	198	neeq1d 2998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅))
200	193, 199	imbi12d 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅)))
201	200, 86	chvarvv 2000	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅)
202	42	hausflf2 23722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
203	182, 190, 191, 201, 202	syl31anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
204		en1b 9025	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
205	203, 204	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
206	205	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
207	109	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
208		flfval 23714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
209	207, 190, 191, 208	syl3anc 1369	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
210	209	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
211	32	uniexd 7734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∪ 𝐾 ∈ V)
212	211	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ∪ 𝐾 ∈ V)
213	42, 212	eqeltrid 2835	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → 𝐵 ∈ V)
214	190	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴))
215		filfbas 23572	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (fBas‘𝐴))
216	214, 215	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (fBas‘𝐴))
217	36	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → 𝐹:𝐴⟶𝐵)
218		simpr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
219		fgfil 23599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
220	190, 219	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
221	220	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
222	218, 221	eleqtrrd 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
223		eqid 2730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
224	223	imaelfm 23675	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
225	213, 216, 217, 222, 224	syl31anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
226		flimclsi 23702	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
227	225, 226	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
228	210, 227	eqsstrd 4019	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
229	206, 228	eqsstrrd 4020	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
230		fvex 6903	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ V
231	230	uniex 7733	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ V
232	231	snss 4788	. . . . . . . . . . . . . . 15 ⊢ (∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ↔ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
233	229, 232	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
234	181, 233	eqeltrd 2831	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
235	166, 172, 179, 234	syl21anc 834	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
236	235	adantlr 711	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
237	165, 236	sseldd 3982	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
238	237	ralrimiva 3144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
239	238	expl 456	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
240	239	reximdv 3168	. . . . . . 7 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
241	240	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
242	164, 241	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
243	65, 42, 4, 32, 36, 69, 76, 86	cnextf 23790	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵)
244	243	ffund 6720	. . . . . . . . 9 ⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
245	244	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
246	65	neii1 22830	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
247	4, 246	sylan 578	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
248	243	fdmd 6727	. . . . . . . . . 10 ⊢ (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
249	248	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
250	247, 249	sseqtrrd 4022	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
251		funimass4 6955	. . . . . . . 8 ⊢ ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252	245, 250, 251	syl2anc 582	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
253	252	biimprd 247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
254	253	reximdva 3166	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
255	1, 242, 254	sylc 65	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
256	255	ralrimiva 3144	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
257	256	ralrimiva 3144	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
258	65, 42	cnnei 23006	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
259	4, 34, 243, 258	syl3anc 1369	. 2 ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
260	257, 259	mpbird 256	1 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 Vcvv 3472 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 {csn 4627 ∪ cuni 4907 class class class wbr 5147 dom cdm 5675 ran crn 5676 “ cima 5678 Fun wfun 6536 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 1_oc1o 8461 ≈ cen 8938 ↾_t crest 17370 fBascfbas 21132 filGencfg 21133 Topctop 22615 TopOnctopon 22632 clsccl 22742 neicnei 22821 Cn ccn 22948 Hauscha 23032 Regcreg 23033 Filcfil 23569 FilMap cfm 23657 fLim cflim 23658 fLimf cflf 23659 CnExtccnext 23783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-1o 8468 df-map 8824 df-pm 8825 df-en 8942 df-rest 17372 df-topgen 17393 df-fbas 21141 df-fg 21142 df-top 22616 df-topon 22633 df-cld 22743 df-ntr 22744 df-cls 22745 df-nei 22822 df-cn 22951 df-cnp 22952 df-haus 23039 df-reg 23040 df-fil 23570 df-fm 23662 df-flim 23663 df-flf 23664 df-cnext 23784

This theorem is referenced by: cnextucn 24028

W3C validator