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 22820

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 767	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝜑)
2		simpll 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝜑)
3		simpr3 1197	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
4		cnextf.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Top)
5	4	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝐽 ∈ Top)
6		simpr2 1196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → 𝑑 ∈ ((nei‘𝐽)‘{𝑥}))
7		neii2 21861	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
8	5, 6, 7	syl2anc 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))
9		vex 3402	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
10	9	snss 4674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑣 ↔ {𝑥} ⊆ 𝑣)
11	10	biimpri 231	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑥} ⊆ 𝑣 → 𝑥 ∈ 𝑣)
12	11	anim1i 618	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))
13	12	anim2i 620	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
14	13	anim2i 620	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
15	14	ex 416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))))
16		3anass 1096	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)))
17	16	anbi1i 627	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑))
18		anass 472	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)))
19		anass 472	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑)))
20	19	anbi2i 626	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑)) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
21	17, 18, 20	3bitri 300	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) ↔ (𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))))
22		opnneip 21872	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
23	4, 22	syl3an1 1164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
24	23	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → 𝑣 ∈ ((nei‘𝐽)‘{𝑥}))
25		simpr2 1196	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ⊆ 𝑑 ∧ (𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣)) → 𝑣 ∈ 𝐽)
26	25	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ⊆ 𝑑 → ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝐽))
27	26	imdistanri 573	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))
28	24, 27	jca 515	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑥 ∈ 𝑣) ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
29	21, 28	sylbir 238	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐽 ∧ (𝑥 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑑))) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)))
30	15, 29	syl6 35	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
31	30	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑))))
32		cnextf.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ Haus)
33		haustop 22084	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Top)
35		imassrn 5914	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ ran 𝐹
36		cnextf.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
37	36	frnd 6512	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
38	35, 37	sstrid 3888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵)
39		ssrin 4124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ⊆ 𝑑 → (𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴))
40		imass2 5939	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∩ 𝐴) ⊆ (𝑑 ∩ 𝐴) → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
41	39, 40	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ⊆ 𝑑 → (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴)))
42		cnextf.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 = ∪ 𝐾
43	42	clsss 21807	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Top ∧ (𝐹 “ (𝑑 ∩ 𝐴)) ⊆ 𝐵 ∧ (𝐹 “ (𝑣 ∩ 𝐴)) ⊆ (𝐹 “ (𝑑 ∩ 𝐴))) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
44	34, 38, 41, 43	syl2an3an 1423	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
45		sstr 3885	. . . . . . . . . . . . . . . . 17 ⊢ ((((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
46	44, 45	sylan 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑣 ⊆ 𝑑) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
47	46	an32s 652	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑣 ⊆ 𝑑) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
48	47	ex 416	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (𝑣 ⊆ 𝑑 → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
49	48	anim2d 615	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑) → (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
50	49	anim2d 615	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
51	31, 50	syld 47	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ((𝑣 ∈ 𝐽 ∧ ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → (𝑣 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))))
52	51	reximdv2 3181	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → (∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)))
53	52	imp 410	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) ∧ ∃𝑣 ∈ 𝐽 ({𝑥} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑑)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
54	2, 3, 8, 53	syl21anc 837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ (𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥}) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
55	54	3anassrs 1361	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑑 ∈ ((nei‘𝐽)‘{𝑥})) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
56		simpr 488	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
57		simp-4l 783	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝜑)
58		simplr 769	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) ∧ ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤) → 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))
59		imaeq2 5899	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (𝐹 “ 𝑢) = (𝐹 “ (𝑑 ∩ 𝐴)))
60	59	fveq2d 6680	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) = ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))))
61	60	sseq1d 3908	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑑 ∩ 𝐴) → (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 ↔ ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
62	61	biimpcd 252	. . . . . . . . . . 11 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (𝑢 = (𝑑 ∩ 𝐴) → ((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
63	62	reximdv 3183	. . . . . . . . . 10 ⊢ (((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤 → (∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤))
64		fvexd 6691	. . . . . . . . . . . 12 ⊢ (𝜑 → ((nei‘𝐽)‘{𝑥}) ∈ V)
65		cnextf.1	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = ∪ 𝐽
66	65	toptopon 21670	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶))
67	4, 66	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶))
68	67	elfvexd 6710	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ V)
69		cnextf.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
70	68, 69	ssexd 5192	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ V)
71		elrest 16806	. . . . . . . . . . . 12 ⊢ ((((nei‘𝐽)‘{𝑥}) ∈ V ∧ 𝐴 ∈ V) → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
72	64, 70, 71	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ↔ ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴)))
73	72	biimpa 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})𝑢 = (𝑑 ∩ 𝐴))
74	63, 73	impel 509	. . . . . . . . 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 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
78	77	anbi2d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶)))
79		sneq 4526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
80	79	fveq2d 6680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦}))
81	80	oveq1d 7187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))
82	81	oveq2d 7188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴)))
83	82	fveq1d 6678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹))
84	83	neeq1d 2993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅))
85	78, 84	imbi12d 348	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅)))
86		cnextf.7	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅)
87	85, 86	chvarvv 2010	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾_t 𝐴))‘𝐹) ≠ ∅)
88	65, 42, 4, 32, 36, 69, 76, 87	cnextfvval 22818	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
89		fvex 6689	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ V
90	89	uniex 7487	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ V
91	90	snid 4552	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)}
92	32	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ Haus)
93	76	eleq2d 2818	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑥 ∈ 𝐶))
94	93	biimpar 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ((cls‘𝐽)‘𝐴))
95	67	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
96	69	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
97		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶)
98		trnei 22645	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
99	95, 96, 97, 98	syl3anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
100	94, 99	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) ∈ (Fil‘𝐴))
101	36	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
102	42	hausflf2 22751	. . . . . . . . . . . . . . . . . 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 8626	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≈ 1_o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)})
105	103, 104	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹)})
106	91, 105	eleqtrrid 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
107	88, 106	eqeltrd 2833	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹))
108	42	toptopon 21670	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵))
109	34, 108	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵))
110	109	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
111		flfnei 22744	. . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝐵 ∧ ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏))
114	113	simprd 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)(𝐹 “ 𝑢) ⊆ 𝑏)
115	114	r19.21bi 3121	. . . . . . . . . . 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 769	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
119	42	neii1 21859	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑏 ⊆ 𝐵)
120	117, 118, 119	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → 𝑏 ⊆ 𝐵)
121		simpr 488	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
122	42	clsss 21807	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏))
123		sstr 3885	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ ((cls‘𝐾)‘𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
124	122, 123	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ (𝐹 “ 𝑢) ⊆ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
125	124	3an1rs 1360	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ∧ (𝐹 “ 𝑢) ⊆ 𝑏) → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
126	125	ex 416	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ⊆ 𝐵 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ((𝐹 “ 𝑢) ⊆ 𝑏 → ((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤))
127	126	reximdv 3183	. . . . . . . . . . . 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 769	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → 𝑐 ∈ 𝐾)
136		simprl 771	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐)
137		regsep 22087	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Reg ∧ 𝑐 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
138	134, 135, 136, 137	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) ∧ 𝑐 ∈ 𝐾) ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤)) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐))
139		sstr 3885	. . . . . . . . . . . . . . . 16 ⊢ ((((cls‘𝐾)‘𝑏) ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((cls‘𝐾)‘𝑏) ⊆ 𝑤)
140	139	expcom 417	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ 𝑤 → (((cls‘𝐾)‘𝑏) ⊆ 𝑐 → ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
141	140	anim2d 615	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ 𝑤 → (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑐) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
142	141	reximdv 3183	. . . . . . . . . . . . 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 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
146		neii2 21861	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
147		fvex 6689	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ V
148	147	snss 4674	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ↔ {(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐)
149	148	anbi1i 627	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤) ↔ ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤))
150	149	biimpri 231	. . . . . . . . . . . . . 14 ⊢ (({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
151	150	reximi 3157	. . . . . . . . . . . . 13 ⊢ (∃𝑐 ∈ 𝐾 ({(((𝐽CnExt𝐾)‘𝐹)‘𝑥)} ⊆ 𝑐 ∧ 𝑐 ⊆ 𝑤) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
152	146, 151	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
153	131, 145, 152	syl2anc 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑐 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑐 ∧ 𝑐 ⊆ 𝑤))
154	144, 153	r19.29a 3199	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤))
155		anass 472	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) ↔ (𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
156		opnneip 21872	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}))
157	156	3expib 1123	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) → 𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})))
158	157	anim1d 614	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Top → (((𝑏 ∈ 𝐾 ∧ (((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
159	155, 158	syl5bir 246	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Top → ((𝑏 ∈ 𝐾 ∧ ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)) → (𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)}) ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤)))
160	159	reximdv2 3181	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → (∃𝑏 ∈ 𝐾 ((((𝐽CnExt𝐾)‘𝐹)‘𝑥) ∈ 𝑏 ∧ ((cls‘𝐾)‘𝑏) ⊆ 𝑤) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤))
161	131, 154, 160	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑏 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})((cls‘𝐾)‘𝑏) ⊆ 𝑤)
162	130, 161	r19.29a 3199	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑢 ∈ (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)((cls‘𝐾)‘(𝐹 “ 𝑢)) ⊆ 𝑤)
163	75, 162	r19.29a 3199	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑑 ∈ ((nei‘𝐽)‘{𝑥})((cls‘𝐾)‘(𝐹 “ (𝑑 ∩ 𝐴))) ⊆ 𝑤)
164	55, 163	r19.29a 3199	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤))
165		simplr 769	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤)
166		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝜑)
167	4	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐽 ∈ Top)
168		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ 𝐽)
169	65	eltopss 21660	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝐶)
170	167, 168, 169	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ⊆ 𝐶)
171		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝑣)
172	170, 171	sseldd 3878	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑧 ∈ 𝐶)
173		fvexd 6691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → ((nei‘𝐽)‘{𝑧}) ∈ V)
174	70	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝐴 ∈ V)
175		opnneip 21872	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
176	4, 175	syl3an1 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
177	176	3expa 1119	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ 𝑧 ∈ 𝑣) → 𝑣 ∈ ((nei‘𝐽)‘{𝑧}))
178		elrestr 16807	. . . . . . . . . . . . . 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 22818	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
181	180	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
182	32	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ Haus)
183	76	eleq2d 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ 𝑧 ∈ 𝐶))
184	183	biimpar 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
185	67	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐽 ∈ (TopOn‘𝐶))
186	69	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐴 ⊆ 𝐶)
187		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶)
188		trnei 22645	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
189	185, 186, 187, 188	syl3anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝑧 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴)))
190	184, 189	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴))
191	36	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐹:𝐴⟶𝐵)
192		eleq1w 2815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶))
193	192	anbi2d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑧 ∈ 𝐶)))
194		sneq 4526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧})
195	194	fveq2d 6680	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑧 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑧}))
196	195	oveq1d 7187	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑧 → (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
197	196	oveq2d 7188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑧 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
198	197	fveq1d 6678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹))
199	198	neeq1d 2993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑧 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅))
200	193, 199	imbi12d 348	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾_t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅)))
201	200, 86	chvarvv 2010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≠ ∅)
202	42	hausflf2 22751	. . . . . . . . . . . . . . . . . . 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 8626	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ≈ 1_o ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
205	203, 204	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
206	205	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)})
207	109	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → 𝐾 ∈ (TopOn‘𝐵))
208		flfval 22743	. . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) = (𝐾 fLim ((𝐵 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))))
211	32	uniexd 7488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∪ 𝐾 ∈ V)
212	211	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ∪ 𝐾 ∈ V)
213	42, 212	eqeltrid 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → 𝐵 ∈ V)
214	190	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴))
215		filfbas 22601	. . . . . . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
219		fgfil 22628	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((nei‘𝐽)‘{𝑧}) ↾_t 𝐴) ∈ (Fil‘𝐴) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
220	190, 219	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
221	220	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
222	218, 221	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → (𝑣 ∩ 𝐴) ∈ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)))
223		eqid 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) = (𝐴filGen(((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))
224	223	imaelfm 22704	. . . . . . . . . . . . . . . . . . 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 22731	. . . . . . . . . . . . . . . . . 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 3915	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
229	206, 228	eqsstrrd 3916	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
230		fvex 6689	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ V
231	230	uniex 7487	. . . . . . . . . . . . . . . 16 ⊢ ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ V
232	231	snss 4674	. . . . . . . . . . . . . . 15 ⊢ (∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ↔ {∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹)} ⊆ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
233	229, 232	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐶) ∧ (𝑣 ∩ 𝐴) ∈ (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴)) → ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑧}) ↾_t 𝐴))‘𝐹) ∈ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))))
234	181, 233	eqeltrd 2833	. . . . . . . . . . . . 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 3878	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) ∧ 𝑧 ∈ 𝑣) → (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
238	237	ralrimiva 3096	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽) ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤)
239	238	expl 461	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ 𝐽 ∧ ((cls‘𝐾)‘(𝐹 “ (𝑣 ∩ 𝐴))) ⊆ 𝑤) → ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
240	239	reximdv 3183	. . . . . . 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 22819	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵)
244	243	ffund 6508	. . . . . . . . 9 ⊢ (𝜑 → Fun ((𝐽CnExt𝐾)‘𝐹))
245	244	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → Fun ((𝐽CnExt𝐾)‘𝐹))
246	65	neii1 21859	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
247	4, 246	sylan 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ 𝐶)
248	243	fdmd 6515	. . . . . . . . . 10 ⊢ (𝜑 → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
249	248	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → dom ((𝐽CnExt𝐾)‘𝐹) = 𝐶)
250	247, 249	sseqtrrd 3918	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹))
251		funimass4 6736	. . . . . . . 8 ⊢ ((Fun ((𝐽CnExt𝐾)‘𝐹) ∧ 𝑣 ⊆ dom ((𝐽CnExt𝐾)‘𝐹)) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
252	245, 250, 251	syl2anc 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → ((((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤))
253	252	biimprd 251	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ ((nei‘𝐽)‘{𝑥})) → (∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → (((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
254	253	reximdva 3184	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})∀𝑧 ∈ 𝑣 (((𝐽CnExt𝐾)‘𝐹)‘𝑧) ∈ 𝑤 → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤))
255	1, 242, 254	sylc 65	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})) → ∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
256	255	ralrimiva 3096	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
257	256	ralrimiva 3096	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑤 ∈ ((nei‘𝐾)‘{(((𝐽CnExt𝐾)‘𝐹)‘𝑥)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑥})(((𝐽CnExt𝐾)‘𝐹) “ 𝑣) ⊆ 𝑤)
258	65, 42	cnnei 22035	. . 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 260	1 ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ≠ wne 2934 ∀wral 3053 ∃wrex 3054 Vcvv 3398 ∩ cin 3842 ⊆ wss 3843 ∅c0 4211 {csn 4516 ∪ cuni 4796 class class class wbr 5030 dom cdm 5525 ran crn 5526 “ cima 5528 Fun wfun 6333 ⟶wf 6335 ‘cfv 6339 (class class class)co 7172 1_oc1o 8126 ≈ cen 8554 ↾_t crest 16799 fBascfbas 20207 filGencfg 20208 Topctop 21646 TopOnctopon 21663 clsccl 21771 neicnei 21850 Cn ccn 21977 Hauscha 22061 Regcreg 22062 Filcfil 22598 FilMap cfm 22686 fLim cflim 22687 fLimf cflf 22688 CnExtccnext 22812

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7481

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-ov 7175 df-oprab 7176 df-mpo 7177 df-1st 7716 df-2nd 7717 df-1o 8133 df-map 8441 df-pm 8442 df-en 8558 df-rest 16801 df-topgen 16822 df-fbas 20216 df-fg 20217 df-top 21647 df-topon 21664 df-cld 21772 df-ntr 21773 df-cls 21774 df-nei 21851 df-cn 21980 df-cnp 21981 df-haus 22068 df-reg 22069 df-fil 22599 df-fm 22691 df-flim 22692 df-flf 22693 df-cnext 22813

This theorem is referenced by: cnextucn 23057

W3C validator