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 24076

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 766	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2		simpll 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝜑)
3		simpr3 1196	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
4		cnextf.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Top)
5	4	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6		simpr2 1195	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7		neii2 23117	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
8	5, 6, 7	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
9		vex 3483	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
10	9	snss 4784	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑣 ↔ {𝑥} ⊆ 𝑣)
11	10	biimpri 228	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑥} ⊆ 𝑣 → 𝑥 ∈ 𝑣)
12	11	anim1i 615	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))
13	12	anim2i 617	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
14	13	anim2i 617	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
15	14	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))))
16		3anass 1094	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)))
17	16	anbi1i 624	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑))
18		anass 468	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)))
19		anass 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
20	19	anbi2i 623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
21	17, 18, 20	3bitri 297	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
22		opnneip 23128	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
23	4, 22	syl3an1 1163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
24	23	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25		simpr2 1195	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ⊆ 𝑑 ∧ (𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) → 𝑣 ∈ 𝐽)
26	25	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ⊆ 𝑑 → ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝐽))
27	26	imdistanri 569	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))
28	24, 27	jca 511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
29	21, 28	sylbir 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
30	15, 29	syl6 35	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
31	30	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
32		cnextf.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Haus)
33		haustop 23340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Top)
35		imassrn 6088	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ ran 𝐹
36		cnextf.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
37	36	frnd 6743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
38	35, 37	sstrid 3994	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵)
39		ssrin 4241	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ⊆ 𝑑 → (𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴))
40		imass2 6119	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ⊆ 𝑑 → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
42		cnextf.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 = ∪ 𝐾
43	42	clsss 23063	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
44	34, 38, 41, 43	syl2an3an 1423	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
45		sstr 3991	. . . . . . . . . . . . . . . . 17 ⊢ ((((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
46	44, 45	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ⊆ 𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
47	46	an32s 652	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
48	47	ex 412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (𝑣 ⊆ 𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
49	48	anim2d 612	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
50	49	anim2d 612	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
51	31, 50	syld 47	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
52	51	reximdv2 3163	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
53	52	imp 406	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
54	2, 3, 8, 53	syl21anc 837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
55	54	3anassrs 1360	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
56		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
57		simp-4l 782	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝜑)
58		simplr 768	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))
59		imaeq2 6073	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (𝐹 “ 𝑢) = (𝐹 “ (𝑑 ∩ 𝐴)))
60	59	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
61	60	sseq1d 4014	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
62	61	biimpcd 249	. . . . . . . . . . 11 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
63	62	reximdv 3169	. . . . . . . . . 10 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
64		fvexd 6920	. . . . . . . . . . . 12 ⊢ (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65		cnextf.1	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = ∪ 𝐽
66	65	toptopon 22924	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
67	4, 66	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶))
68	67	elfvexd 6944	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ V)
69		cnextf.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
70	68, 69	ssexd 5323	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ V)
71		elrest 17473	. . . . . . . . . . . 12 ⊢ ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
72	64, 70, 71	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
73	72	biimpa 476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴))
74	63, 73	impel 505	. . . . . . . . 9 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ∧ (𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
75	56, 57, 58, 74	syl12anc 836	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
76		cnextf.6	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)
77		eleq1w 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
78	77	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶)))
79		sneq 4635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
80	79	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
81	80	oveq1d 7447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))
82	81	oveq2d 7448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴)))
83	82	fveq1d 6907	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹))
84	83	neeq1d 2999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅))
85	78, 84	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅)))
86		cnextf.7	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅)
87	85, 86	chvarvv 1997	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅)
88	65, 42, 4, 32, 36, 69, 76, 87	cnextfvval 24074	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
89		fvex 6918	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ V
90	89	uniex 7762	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ V
91	90	snid 4661	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)}
92	32	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ Haus)
93	76	eleq2d 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶))
94	93	biimpar 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
95	67	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
96	69	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
97		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶)
98		trnei 23901	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
99	95, 96, 97, 98	syl3anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
100	94, 99	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴))
101	36	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
102	42	hausflf2 24007	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
103	92, 100, 101, 86, 102	syl31anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
104		en1b 9066	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)})
105	103, 104	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)})
106	91, 105	eleqtrrid 2847	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
107	88, 106	eqeltrd 2840	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
108	42	toptopon 22924	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
109	34, 108	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵))
110	109	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
111		flfnei 24000	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)))
112	110, 100, 101, 111	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ↔ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)))
113	107, 112	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏))
114	113	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
115	114	r19.21bi 3250	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
116	115	ad4ant13 751	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
117	34	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝐾 ∈ Top)
118		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
119	42	neii1 23115	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏 ⊆ 𝐵)
120	117, 118, 119	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ⊆ 𝐵)
121		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
122	42	clsss 23063	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
123		sstr 3991	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
124	122, 123	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
125	124	3an1rs 1359	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
126	125	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹 “ 𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
127	126	reximdv 3169	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
128	117, 120, 121, 127	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏 → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
129	128	adantllr 719	. . . . . . . . . 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 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Top)
132		cnextcn.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Reg)
133	132	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝐾 ∈ Reg)
134	133	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝐾 ∈ Reg)
135		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝑐 ∈ 𝐾)
136		simprl 770	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
137		regsep 23343	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
138	134, 135, 136, 137	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
139		sstr 3991	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘𝑏) ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
140	139	expcom 413	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ 𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
141	140	anim2d 612	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ 𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
142	141	reximdv 3169	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ 𝑤 → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
143	142	ad2antll 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
144	138, 143	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
145		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
146		neii2 23117	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
147		fvex 6918	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
148	147	snss 4784	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
149	148	anbi1i 624	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
150	149	biimpri 228	. . . . . . . . . . . . . 14 ⊢ (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
151	150	reximi 3083	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
152	146, 151	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
153	131, 145, 152	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
154	144, 153	r19.29a 3161	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
155		anass 468	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
156		opnneip 23128	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
157	156	3expib 1122	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
158	157	anim1d 611	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Top → (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
159	155, 158	biimtrrid 243	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
160	159	reximdv2 3163	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
161	131, 154, 160	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
162	130, 161	r19.29a 3161	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
163	75, 162	r19.29a 3161	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
164	55, 163	r19.29a 3161	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
165		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
166		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝜑)
167	4	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐽 ∈ Top)
168		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ 𝐽)
169	65	eltopss 22914	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝐶)
170	167, 168, 169	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ⊆ 𝐶)
171		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝑣)
172	170, 171	sseldd 3983	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝐶)
173		fvexd 6920	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
174	70	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐴 ∈ V)
175		opnneip 23128	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
176	4, 175	syl3an1 1163	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
177	176	3expa 1118	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
178		elrestr 17474	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑧})) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
179	173, 174, 177, 178	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
180	65, 42, 4, 32, 36, 69, 76, 86	cnextfvval 24074	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
181	180	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
182	32	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ Haus)
183	76	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧 ∈ 𝐶))
184	183	biimpar 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
185	67	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
186	69	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
187		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶)
188		trnei 23901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
189	185, 186, 187, 188	syl3anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
190	184, 189	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴))
191	36	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
192		eleq1w 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶))
193	192	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑧 ∈ 𝐶)))
194		sneq 4635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧})
195	194	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
196	195	oveq1d 7447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
197	196	oveq2d 7448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
198	197	fveq1d 6907	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
199	198	neeq1d 2999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅))
200	193, 199	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅)))
201	200, 86	chvarvv 1997	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅)
202	42	hausflf2 24007	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾 ∈ Haus ∧ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
203	182, 190, 191, 201, 202	syl31anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o)
204		en1b 9066	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
205	203, 204	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
206	205	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
207	109	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
208		flfval 23999	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
209	207, 190, 191, 208	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
210	209	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
211	32	uniexd 7763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∪ 𝐾 ∈ V)
212	211	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ∪ 𝐾 ∈ V)
213	42, 212	eqeltrid 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → 𝐵 ∈ V)
214	190	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴))
215		filfbas 23857	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (fBas‘𝐴))
216	214, 215	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (fBas‘𝐴))
217	36	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → 𝐹:𝐴⟶𝐵)
218		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
219		fgfil 23884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
220	190, 219	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
221	220	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
222	218, 221	eleqtrrd 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
223		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
224	223	imaelfm 23960	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ V ∧ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
225	213, 216, 217, 222, 224	syl31anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐹 “ (𝑣 ∩ 𝐴)) ∈ ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
226		flimclsi 23987	. . . . . . . . . . . . . . . . . 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 4017	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
229	206, 228	eqsstrrd 4018	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
230		fvex 6918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ V
231	230	uniex 7762	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ V
232	231	snss 4784	. . . . . . . . . . . . . . 15 ⊢ (∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ↔ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
233	229, 232	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
234	181, 233	eqeltrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
235	166, 172, 179, 234	syl21anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
236	235	adantlr 715	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
237	165, 236	sseldd 3983	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
238	237	ralrimiva 3145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
239	238	expl 457	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
240	239	reximdv 3169	. . . . . . 7 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
241	240	ad2antrr 726	. . . . . 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 24075	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵)
244	243	ffund 6739	. . . . . . . . 9 ⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
245	244	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
246	65	neii1 23115	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
247	4, 246	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
248	243	fdmd 6745	. . . . . . . . . 10 ⊢ (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
249	248	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
250	247, 249	sseqtrrd 4020	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
251		funimass4 6972	. . . . . . . 8 ⊢ ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252	245, 250, 251	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
253	252	biimprd 248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
254	253	reximdva 3167	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
255	1, 242, 254	sylc 65	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
256	255	ralrimiva 3145	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
257	256	ralrimiva 3145	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
258	65, 42	cnnei 23291	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
259	4, 34, 243, 258	syl3anc 1372	. 2 ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
260	257, 259	mpbird 257	1 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 Vcvv 3479 ∩ cin 3949 ⊆ wss 3950 ∅c0 4332 {csn 4625 ∪ cuni 4906 class class class wbr 5142 dom cdm 5684 ran crn 5685 “ cima 5687 Fun wfun 6554 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 1_oc1o 8500 ≈ cen 8983 ↾_t crest 17466 fBascfbas 21353 filGencfg 21354 Topctop 22900 TopOnctopon 22917 clsccl 23027 neicnei 23106 Cn ccn 23233 Hauscha 23317 Regcreg 23318 Filcfil 23854 FilMap cfm 23942 fLim cflim 23943 fLimf cflf 23944 CnExtccnext 24068

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-iin 4993 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-ov 7435 df-oprab 7436 df-mpo 7437 df-1st 8015 df-2nd 8016 df-1o 8507 df-map 8869 df-pm 8870 df-en 8987 df-rest 17468 df-topgen 17489 df-fbas 21362 df-fg 21363 df-top 22901 df-topon 22918 df-cld 23028 df-ntr 23029 df-cls 23030 df-nei 23107 df-cn 23236 df-cnp 23237 df-haus 23324 df-reg 23325 df-fil 23855 df-fm 23947 df-flim 23948 df-flf 23949 df-cnext 24069

This theorem is referenced by: cnextucn 24313

W3C validator