cnextcn

Description: Extension by continuity. Theorem 1 of BourbakiTop1 p. I.57. Given a topology J on C , a subset A dense in C , this states a condition for F from A to a regular space K to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018)

	Ref	Expression
Hypotheses	cnextf.1	$⊢ C = ⋃ J$
	cnextf.2	$⊢ B = ⋃ K$
	cnextf.3	$⊢ φ \to J \in Top$
	cnextf.4	$⊢ φ \to K \in Haus$
	cnextf.5	$⊢ φ \to F : A ⟶ B$
	cnextf.a	$⊢ φ \to A \subseteq C$
	cnextf.6	$⊢ φ \to cls (J) (A) = C$
	cnextf.7	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
	cnextcn.8	$⊢ φ \to K \in Reg$
Assertion	cnextcn	$⊢ φ \to (J CnExt K) (F) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		cnextf.1	$⊢ C = ⋃ J$
2		cnextf.2	$⊢ B = ⋃ K$
3		cnextf.3	$⊢ φ \to J \in Top$
4		cnextf.4	$⊢ φ \to K \in Haus$
5		cnextf.5	$⊢ φ \to F : A ⟶ B$
6		cnextf.a	$⊢ φ \to A \subseteq C$
7		cnextf.6	$⊢ φ \to cls (J) (A) = C$
8		cnextf.7	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
9		cnextcn.8	$⊢ φ \to K \in Reg$
10		simpll	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to φ$
11		simpll	$⊢ ((φ \land x \in C) \land (w \in nei (K) (\{(J CnExt K) (F) (x)\}) \land d \in nei (J) (\{x\}) \land cls (K) (F [d \cap A]) \subseteq w)) \to φ$
12		simpr3	$⊢ ((φ \land x \in C) \land (w \in nei (K) (\{(J CnExt K) (F) (x)\}) \land d \in nei (J) (\{x\}) \land cls (K) (F [d \cap A]) \subseteq w)) \to cls (K) (F [d \cap A]) \subseteq w$
13	3	ad2antrr	$⊢ ((φ \land x \in C) \land (w \in nei (K) (\{(J CnExt K) (F) (x)\}) \land d \in nei (J) (\{x\}) \land cls (K) (F [d \cap A]) \subseteq w)) \to J \in Top$
14		simpr2	$⊢ ((φ \land x \in C) \land (w \in nei (K) (\{(J CnExt K) (F) (x)\}) \land d \in nei (J) (\{x\}) \land cls (K) (F [d \cap A]) \subseteq w)) \to d \in nei (J) (\{x\})$
15		neii2	$⊢ (J \in Top \land d \in nei (J) (\{x\})) \to \exists v \in J (\{x\} \subseteq v \land v \subseteq d)$
16	13 14 15	syl2anc	$⊢ ((φ \land x \in C) \land (w \in nei (K) (\{(J CnExt K) (F) (x)\}) \land d \in nei (J) (\{x\}) \land cls (K) (F [d \cap A]) \subseteq w)) \to \exists v \in J (\{x\} \subseteq v \land v \subseteq d)$
17		vex	$⊢ x \in V$
18	17	snss	$⊢ x \in v \leftrightarrow \{x\} \subseteq v$
19	18	biimpri	$⊢ \{x\} \subseteq v \to x \in v$
20	19	anim1i	$⊢ (\{x\} \subseteq v \land v \subseteq d) \to (x \in v \land v \subseteq d)$
21	20	anim2i	$⊢ (v \in J \land (\{x\} \subseteq v \land v \subseteq d)) \to (v \in J \land (x \in v \land v \subseteq d))$
22	21	anim2i	$⊢ (φ \land (v \in J \land (\{x\} \subseteq v \land v \subseteq d))) \to (φ \land (v \in J \land (x \in v \land v \subseteq d)))$
23	22	ex	$⊢ φ \to ((v \in J \land (\{x\} \subseteq v \land v \subseteq d)) \to (φ \land (v \in J \land (x \in v \land v \subseteq d))))$
24		3anass	$⊢ (φ \land v \in J \land x \in v) \leftrightarrow (φ \land (v \in J \land x \in v))$
25	24	anbi1i	$⊢ ((φ \land v \in J \land x \in v) \land v \subseteq d) \leftrightarrow ((φ \land (v \in J \land x \in v)) \land v \subseteq d)$
26		anass	$⊢ ((φ \land (v \in J \land x \in v)) \land v \subseteq d) \leftrightarrow (φ \land ((v \in J \land x \in v) \land v \subseteq d))$
27		anass	$⊢ ((v \in J \land x \in v) \land v \subseteq d) \leftrightarrow (v \in J \land (x \in v \land v \subseteq d))$
28	27	anbi2i	$⊢ (φ \land ((v \in J \land x \in v) \land v \subseteq d)) \leftrightarrow (φ \land (v \in J \land (x \in v \land v \subseteq d)))$
29	25 26 28	3bitri	$⊢ ((φ \land v \in J \land x \in v) \land v \subseteq d) \leftrightarrow (φ \land (v \in J \land (x \in v \land v \subseteq d)))$
30		opnneip	$⊢ (J \in Top \land v \in J \land x \in v) \to v \in nei (J) (\{x\})$
31	3 30	syl3an1	$⊢ (φ \land v \in J \land x \in v) \to v \in nei (J) (\{x\})$
32	31	adantr	$⊢ ((φ \land v \in J \land x \in v) \land v \subseteq d) \to v \in nei (J) (\{x\})$
33		simpr2	$⊢ (v \subseteq d \land (φ \land v \in J \land x \in v)) \to v \in J$
34	33	ex	$⊢ v \subseteq d \to ((φ \land v \in J \land x \in v) \to v \in J)$
35	34	imdistanri	$⊢ ((φ \land v \in J \land x \in v) \land v \subseteq d) \to (v \in J \land v \subseteq d)$
36	32 35	jca	$⊢ ((φ \land v \in J \land x \in v) \land v \subseteq d) \to (v \in nei (J) (\{x\}) \land (v \in J \land v \subseteq d))$
37	29 36	sylbir	$⊢ (φ \land (v \in J \land (x \in v \land v \subseteq d))) \to (v \in nei (J) (\{x\}) \land (v \in J \land v \subseteq d))$
38	23 37	syl6	$⊢ φ \to ((v \in J \land (\{x\} \subseteq v \land v \subseteq d)) \to (v \in nei (J) (\{x\}) \land (v \in J \land v \subseteq d)))$
39	38	adantr	$⊢ (φ \land cls (K) (F [d \cap A]) \subseteq w) \to ((v \in J \land (\{x\} \subseteq v \land v \subseteq d)) \to (v \in nei (J) (\{x\}) \land (v \in J \land v \subseteq d)))$
40		haustop	$⊢ K \in Haus \to K \in Top$
41	4 40	syl	$⊢ φ \to K \in Top$
42		imassrn	$⊢ F [d \cap A] \subseteq ran F$
43	5	frnd	$⊢ φ \to ran F \subseteq B$
44	42 43	sstrid	$⊢ φ \to F [d \cap A] \subseteq B$
45		ssrin	$⊢ v \subseteq d \to v \cap A \subseteq d \cap A$
46		imass2	$⊢ v \cap A \subseteq d \cap A \to F [v \cap A] \subseteq F [d \cap A]$
47	45 46	syl	$⊢ v \subseteq d \to F [v \cap A] \subseteq F [d \cap A]$
48	2	clsss	$⊢ (K \in Top \land F [d \cap A] \subseteq B \land F [v \cap A] \subseteq F [d \cap A]) \to cls (K) (F [v \cap A]) \subseteq cls (K) (F [d \cap A])$
49	41 44 47 48	syl2an3an	$⊢ (φ \land v \subseteq d) \to cls (K) (F [v \cap A]) \subseteq cls (K) (F [d \cap A])$
50		sstr	$⊢ (cls (K) (F [v \cap A]) \subseteq cls (K) (F [d \cap A]) \land cls (K) (F [d \cap A]) \subseteq w) \to cls (K) (F [v \cap A]) \subseteq w$
51	49 50	sylan	$⊢ ((φ \land v \subseteq d) \land cls (K) (F [d \cap A]) \subseteq w) \to cls (K) (F [v \cap A]) \subseteq w$
52	51	an32s	$⊢ ((φ \land cls (K) (F [d \cap A]) \subseteq w) \land v \subseteq d) \to cls (K) (F [v \cap A]) \subseteq w$
53	52	ex	$⊢ (φ \land cls (K) (F [d \cap A]) \subseteq w) \to (v \subseteq d \to cls (K) (F [v \cap A]) \subseteq w)$
54	53	anim2d	$⊢ (φ \land cls (K) (F [d \cap A]) \subseteq w) \to ((v \in J \land v \subseteq d) \to (v \in J \land cls (K) (F [v \cap A]) \subseteq w))$
55	54	anim2d	$⊢ (φ \land cls (K) (F [d \cap A]) \subseteq w) \to ((v \in nei (J) (\{x\}) \land (v \in J \land v \subseteq d)) \to (v \in nei (J) (\{x\}) \land (v \in J \land cls (K) (F [v \cap A]) \subseteq w)))$
56	39 55	syld	$⊢ (φ \land cls (K) (F [d \cap A]) \subseteq w) \to ((v \in J \land (\{x\} \subseteq v \land v \subseteq d)) \to (v \in nei (J) (\{x\}) \land (v \in J \land cls (K) (F [v \cap A]) \subseteq w)))$
57	56	reximdv2	$⊢ (φ \land cls (K) (F [d \cap A]) \subseteq w) \to (\exists v \in J (\{x\} \subseteq v \land v \subseteq d) \to \exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w))$
58	57	imp	$⊢ ((φ \land cls (K) (F [d \cap A]) \subseteq w) \land \exists v \in J (\{x\} \subseteq v \land v \subseteq d)) \to \exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w)$
59	11 12 16 58	syl21anc	$⊢ ((φ \land x \in C) \land (w \in nei (K) (\{(J CnExt K) (F) (x)\}) \land d \in nei (J) (\{x\}) \land cls (K) (F [d \cap A]) \subseteq w)) \to \exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w)$
60	59	3anassrs	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land d \in nei (J) (\{x\})) \land cls (K) (F [d \cap A]) \subseteq w) \to \exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w)$
61		simpr	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land u \in (nei (J) (\{x\}) ↾_{𝑡} A)) \land cls (K) (F [u]) \subseteq w) \to cls (K) (F [u]) \subseteq w$
62		simp-4l	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land u \in (nei (J) (\{x\}) ↾_{𝑡} A)) \land cls (K) (F [u]) \subseteq w) \to φ$
63		simplr	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land u \in (nei (J) (\{x\}) ↾_{𝑡} A)) \land cls (K) (F [u]) \subseteq w) \to u \in (nei (J) (\{x\}) ↾_{𝑡} A)$
64		imaeq2	$⊢ u = d \cap A \to F [u] = F [d \cap A]$
65	64	fveq2d	$⊢ u = d \cap A \to cls (K) (F [u]) = cls (K) (F [d \cap A])$
66	65	sseq1d	$⊢ u = d \cap A \to (cls (K) (F [u]) \subseteq w \leftrightarrow cls (K) (F [d \cap A]) \subseteq w)$
67	66	biimpcd	$⊢ cls (K) (F [u]) \subseteq w \to (u = d \cap A \to cls (K) (F [d \cap A]) \subseteq w)$
68	67	reximdv	$⊢ cls (K) (F [u]) \subseteq w \to (\exists d \in nei (J) (\{x\}) u = d \cap A \to \exists d \in nei (J) (\{x\}) cls (K) (F [d \cap A]) \subseteq w)$
69		fvexd	$⊢ φ \to nei (J) (\{x\}) \in V$
70	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (C)$
71	3 70	sylib	$⊢ φ \to J \in TopOn (C)$
72	71	elfvexd	$⊢ φ \to C \in V$
73	72 6	ssexd	$⊢ φ \to A \in V$
74		elrest	$⊢ (nei (J) (\{x\}) \in V \land A \in V) \to (u \in (nei (J) (\{x\}) ↾_{𝑡} A) \leftrightarrow \exists d \in nei (J) (\{x\}) u = d \cap A)$
75	69 73 74	syl2anc	$⊢ φ \to (u \in (nei (J) (\{x\}) ↾_{𝑡} A) \leftrightarrow \exists d \in nei (J) (\{x\}) u = d \cap A)$
76	75	biimpa	$⊢ (φ \land u \in (nei (J) (\{x\}) ↾_{𝑡} A)) \to \exists d \in nei (J) (\{x\}) u = d \cap A$
77	68 76	impel	$⊢ (cls (K) (F [u]) \subseteq w \land (φ \land u \in (nei (J) (\{x\}) ↾_{𝑡} A))) \to \exists d \in nei (J) (\{x\}) cls (K) (F [d \cap A]) \subseteq w$
78	61 62 63 77	syl12anc	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land u \in (nei (J) (\{x\}) ↾_{𝑡} A)) \land cls (K) (F [u]) \subseteq w) \to \exists d \in nei (J) (\{x\}) cls (K) (F [d \cap A]) \subseteq w$
79		eleq1w	$⊢ x = y \to (x \in C \leftrightarrow y \in C)$
80	79	anbi2d	$⊢ x = y \to ((φ \land x \in C) \leftrightarrow (φ \land y \in C))$
81		sneq	$⊢ x = y \to \{x\} = \{y\}$
82	81	fveq2d	$⊢ x = y \to nei (J) (\{x\}) = nei (J) (\{y\})$
83	82	oveq1d	$⊢ x = y \to nei (J) (\{x\}) ↾_{𝑡} A = nei (J) (\{y\}) ↾_{𝑡} A$
84	83	oveq2d	$⊢ x = y \to K fLimf (nei (J) (\{x\}) ↾_{𝑡} A) = K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)$
85	84	fveq1d	$⊢ x = y \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F)$
86	85	neeq1d	$⊢ x = y \to ((K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset \leftrightarrow (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset)$
87	80 86	imbi12d	$⊢ x = y \to (((φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset) \leftrightarrow ((φ \land y \in C) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset))$
88	87 8	chvarvv	$⊢ (φ \land y \in C) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset$
89	1 2 3 4 5 6 7 88	cnextfvval	$⊢ (φ \land x \in C) \to (J CnExt K) (F) (x) = ⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
90		fvex	$⊢ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \in V$
91	90	uniex	$⊢ ⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \in V$
92	91	snid	$⊢ ⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \in \{⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)\}$
93	4	adantr	$⊢ (φ \land x \in C) \to K \in Haus$
94	7	eleq2d	$⊢ φ \to (x \in cls (J) (A) \leftrightarrow x \in C)$
95	94	biimpar	$⊢ (φ \land x \in C) \to x \in cls (J) (A)$
96	71	adantr	$⊢ (φ \land x \in C) \to J \in TopOn (C)$
97	6	adantr	$⊢ (φ \land x \in C) \to A \subseteq C$
98		simpr	$⊢ (φ \land x \in C) \to x \in C$
99		trnei	$⊢ (J \in TopOn (C) \land A \subseteq C \land x \in C) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
100	96 97 98 99	syl3anc	$⊢ (φ \land x \in C) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
101	95 100	mpbid	$⊢ (φ \land x \in C) \to nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A)$
102	5	adantr	$⊢ (φ \land x \in C) \to F : A ⟶ B$
103	2	hausflf2	$⊢ ((K \in Haus \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \land (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}$
104	93 101 102 8 103	syl31anc	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}$
105		en1b	$⊢ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜} \leftrightarrow (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = \{⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)\}$
106	104 105	sylib	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = \{⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)\}$
107	92 106	eleqtrrid	$⊢ (φ \land x \in C) \to ⋃ (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
108	89 107	eqeltrd	$⊢ (φ \land x \in C) \to (J CnExt K) (F) (x) \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)$
109	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (B)$
110	41 109	sylib	$⊢ φ \to K \in TopOn (B)$
111	110	adantr	$⊢ (φ \land x \in C) \to K \in TopOn (B)$
112		flfnei	$⊢ (K \in TopOn (B) \land nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \to ((J CnExt K) (F) (x) \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \leftrightarrow ((J CnExt K) (F) (x) \in B \land \forall b \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b))$
113	111 101 102 112	syl3anc	$⊢ (φ \land x \in C) \to ((J CnExt K) (F) (x) \in (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \leftrightarrow ((J CnExt K) (F) (x) \in B \land \forall b \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b))$
114	108 113	mpbid	$⊢ (φ \land x \in C) \to ((J CnExt K) (F) (x) \in B \land \forall b \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b)$
115	114	simprd	$⊢ (φ \land x \in C) \to \forall b \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b$
116	115	r19.21bi	$⊢ ((φ \land x \in C) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b$
117	116	ad4ant13	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b$
118	41	ad3antrrr	$⊢ (((φ \land x \in C) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to K \in Top$
119		simplr	$⊢ (((φ \land x \in C) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to b \in nei (K) (\{(J CnExt K) (F) (x)\})$
120	2	neii1	$⊢ (K \in Top \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \to b \subseteq B$
121	118 119 120	syl2anc	$⊢ (((φ \land x \in C) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to b \subseteq B$
122		simpr	$⊢ (((φ \land x \in C) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to cls (K) (b) \subseteq w$
123	2	clsss	$⊢ (K \in Top \land b \subseteq B \land F [u] \subseteq b) \to cls (K) (F [u]) \subseteq cls (K) (b)$
124		sstr	$⊢ (cls (K) (F [u]) \subseteq cls (K) (b) \land cls (K) (b) \subseteq w) \to cls (K) (F [u]) \subseteq w$
125	123 124	sylan	$⊢ ((K \in Top \land b \subseteq B \land F [u] \subseteq b) \land cls (K) (b) \subseteq w) \to cls (K) (F [u]) \subseteq w$
126	125	3an1rs	$⊢ ((K \in Top \land b \subseteq B \land cls (K) (b) \subseteq w) \land F [u] \subseteq b) \to cls (K) (F [u]) \subseteq w$
127	126	ex	$⊢ (K \in Top \land b \subseteq B \land cls (K) (b) \subseteq w) \to (F [u] \subseteq b \to cls (K) (F [u]) \subseteq w)$
128	127	reximdv	$⊢ (K \in Top \land b \subseteq B \land cls (K) (b) \subseteq w) \to (\exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) cls (K) (F [u]) \subseteq w)$
129	118 121 122 128	syl3anc	$⊢ (((φ \land x \in C) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to (\exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) cls (K) (F [u]) \subseteq w)$
130	129	adantllr	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to (\exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) F [u] \subseteq b \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) cls (K) (F [u]) \subseteq w)$
131	117 130	mpd	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land b \in nei (K) (\{(J CnExt K) (F) (x)\})) \land cls (K) (b) \subseteq w) \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) cls (K) (F [u]) \subseteq w$
132	41	ad2antrr	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to K \in Top$
133	9	ad2antrr	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to K \in Reg$
134	133	ad2antrr	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land c \in K) \land ((J CnExt K) (F) (x) \in c \land c \subseteq w)) \to K \in Reg$
135		simplr	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land c \in K) \land ((J CnExt K) (F) (x) \in c \land c \subseteq w)) \to c \in K$
136		simprl	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land c \in K) \land ((J CnExt K) (F) (x) \in c \land c \subseteq w)) \to (J CnExt K) (F) (x) \in c$
137		regsep	$⊢ (K \in Reg \land c \in K \land (J CnExt K) (F) (x) \in c) \to \exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq c)$
138	134 135 136 137	syl3anc	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land c \in K) \land ((J CnExt K) (F) (x) \in c \land c \subseteq w)) \to \exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq c)$
139		sstr	$⊢ (cls (K) (b) \subseteq c \land c \subseteq w) \to cls (K) (b) \subseteq w$
140	139	expcom	$⊢ c \subseteq w \to (cls (K) (b) \subseteq c \to cls (K) (b) \subseteq w)$
141	140	anim2d	$⊢ c \subseteq w \to (((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq c) \to ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w))$
142	141	reximdv	$⊢ c \subseteq w \to (\exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq c) \to \exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w))$
143	142	ad2antll	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land c \in K) \land ((J CnExt K) (F) (x) \in c \land c \subseteq w)) \to (\exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq c) \to \exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w))$
144	138 143	mpd	$⊢ ((((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \land c \in K) \land ((J CnExt K) (F) (x) \in c \land c \subseteq w)) \to \exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w)$
145		simpr	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to w \in nei (K) (\{(J CnExt K) (F) (x)\})$
146		neii2	$⊢ (K \in Top \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists c \in K (\{(J CnExt K) (F) (x)\} \subseteq c \land c \subseteq w)$
147		fvex	$⊢ (J CnExt K) (F) (x) \in V$
148	147	snss	$⊢ (J CnExt K) (F) (x) \in c \leftrightarrow \{(J CnExt K) (F) (x)\} \subseteq c$
149	148	anbi1i	$⊢ ((J CnExt K) (F) (x) \in c \land c \subseteq w) \leftrightarrow (\{(J CnExt K) (F) (x)\} \subseteq c \land c \subseteq w)$
150	149	biimpri	$⊢ (\{(J CnExt K) (F) (x)\} \subseteq c \land c \subseteq w) \to ((J CnExt K) (F) (x) \in c \land c \subseteq w)$
151	150	reximi	$⊢ \exists c \in K (\{(J CnExt K) (F) (x)\} \subseteq c \land c \subseteq w) \to \exists c \in K ((J CnExt K) (F) (x) \in c \land c \subseteq w)$
152	146 151	syl	$⊢ (K \in Top \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists c \in K ((J CnExt K) (F) (x) \in c \land c \subseteq w)$
153	132 145 152	syl2anc	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists c \in K ((J CnExt K) (F) (x) \in c \land c \subseteq w)$
154	144 153	r19.29a	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w)$
155		anass	$⊢ ((b \in K \land (J CnExt K) (F) (x) \in b) \land cls (K) (b) \subseteq w) \leftrightarrow (b \in K \land ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w))$
156		opnneip	$⊢ (K \in Top \land b \in K \land (J CnExt K) (F) (x) \in b) \to b \in nei (K) (\{(J CnExt K) (F) (x)\})$
157	156	3expib	$⊢ K \in Top \to ((b \in K \land (J CnExt K) (F) (x) \in b) \to b \in nei (K) (\{(J CnExt K) (F) (x)\}))$
158	157	anim1d	$⊢ K \in Top \to (((b \in K \land (J CnExt K) (F) (x) \in b) \land cls (K) (b) \subseteq w) \to (b \in nei (K) (\{(J CnExt K) (F) (x)\}) \land cls (K) (b) \subseteq w))$
159	155 158	syl5bir	$⊢ K \in Top \to ((b \in K \land ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w)) \to (b \in nei (K) (\{(J CnExt K) (F) (x)\}) \land cls (K) (b) \subseteq w))$
160	159	reximdv2	$⊢ K \in Top \to (\exists b \in K ((J CnExt K) (F) (x) \in b \land cls (K) (b) \subseteq w) \to \exists b \in nei (K) (\{(J CnExt K) (F) (x)\}) cls (K) (b) \subseteq w)$
161	132 154 160	sylc	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists b \in nei (K) (\{(J CnExt K) (F) (x)\}) cls (K) (b) \subseteq w$
162	131 161	r19.29a	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists u \in (nei (J) (\{x\}) ↾_{𝑡} A) cls (K) (F [u]) \subseteq w$
163	78 162	r19.29a	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists d \in nei (J) (\{x\}) cls (K) (F [d \cap A]) \subseteq w$
164	60 163	r19.29a	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w)$
165		simplr	$⊢ (((φ \land v \in J) \land cls (K) (F [v \cap A]) \subseteq w) \land z \in v) \to cls (K) (F [v \cap A]) \subseteq w$
166		simpll	$⊢ ((φ \land v \in J) \land z \in v) \to φ$
167	3	ad2antrr	$⊢ ((φ \land v \in J) \land z \in v) \to J \in Top$
168		simplr	$⊢ ((φ \land v \in J) \land z \in v) \to v \in J$
169	1	eltopss	$⊢ (J \in Top \land v \in J) \to v \subseteq C$
170	167 168 169	syl2anc	$⊢ ((φ \land v \in J) \land z \in v) \to v \subseteq C$
171		simpr	$⊢ ((φ \land v \in J) \land z \in v) \to z \in v$
172	170 171	sseldd	$⊢ ((φ \land v \in J) \land z \in v) \to z \in C$
173		fvexd	$⊢ ((φ \land v \in J) \land z \in v) \to nei (J) (\{z\}) \in V$
174	73	ad2antrr	$⊢ ((φ \land v \in J) \land z \in v) \to A \in V$
175		opnneip	$⊢ (J \in Top \land v \in J \land z \in v) \to v \in nei (J) (\{z\})$
176	3 175	syl3an1	$⊢ (φ \land v \in J \land z \in v) \to v \in nei (J) (\{z\})$
177	176	3expa	$⊢ ((φ \land v \in J) \land z \in v) \to v \in nei (J) (\{z\})$
178		elrestr	$⊢ (nei (J) (\{z\}) \in V \land A \in V \land v \in nei (J) (\{z\})) \to v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)$
179	173 174 177 178	syl3anc	$⊢ ((φ \land v \in J) \land z \in v) \to v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)$
180	1 2 3 4 5 6 7 8	cnextfvval	$⊢ (φ \land z \in C) \to (J CnExt K) (F) (z) = ⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)$
181	180	adantr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to (J CnExt K) (F) (z) = ⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)$
182	4	adantr	$⊢ (φ \land z \in C) \to K \in Haus$
183	7	eleq2d	$⊢ φ \to (z \in cls (J) (A) \leftrightarrow z \in C)$
184	183	biimpar	$⊢ (φ \land z \in C) \to z \in cls (J) (A)$
185	71	adantr	$⊢ (φ \land z \in C) \to J \in TopOn (C)$
186	6	adantr	$⊢ (φ \land z \in C) \to A \subseteq C$
187		simpr	$⊢ (φ \land z \in C) \to z \in C$
188		trnei	$⊢ (J \in TopOn (C) \land A \subseteq C \land z \in C) \to (z \in cls (J) (A) \leftrightarrow nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A))$
189	185 186 187 188	syl3anc	$⊢ (φ \land z \in C) \to (z \in cls (J) (A) \leftrightarrow nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A))$
190	184 189	mpbid	$⊢ (φ \land z \in C) \to nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A)$
191	5	adantr	$⊢ (φ \land z \in C) \to F : A ⟶ B$
192		eleq1w	$⊢ x = z \to (x \in C \leftrightarrow z \in C)$
193	192	anbi2d	$⊢ x = z \to ((φ \land x \in C) \leftrightarrow (φ \land z \in C))$
194		sneq	$⊢ x = z \to \{x\} = \{z\}$
195	194	fveq2d	$⊢ x = z \to nei (J) (\{x\}) = nei (J) (\{z\})$
196	195	oveq1d	$⊢ x = z \to nei (J) (\{x\}) ↾_{𝑡} A = nei (J) (\{z\}) ↾_{𝑡} A$
197	196	oveq2d	$⊢ x = z \to K fLimf (nei (J) (\{x\}) ↾_{𝑡} A) = K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)$
198	197	fveq1d	$⊢ x = z \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)$
199	198	neeq1d	$⊢ x = z \to ((K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset \leftrightarrow (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \neq \emptyset)$
200	193 199	imbi12d	$⊢ x = z \to (((φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset) \leftrightarrow ((φ \land z \in C) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \neq \emptyset))$
201	200 8	chvarvv	$⊢ (φ \land z \in C) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \neq \emptyset$
202	2	hausflf2	$⊢ ((K \in Haus \land nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \land (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \neq \emptyset) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}$
203	182 190 191 201 202	syl31anc	$⊢ (φ \land z \in C) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}$
204		en1b	$⊢ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜} \leftrightarrow (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) = \{⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)\}$
205	203 204	sylib	$⊢ (φ \land z \in C) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) = \{⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)\}$
206	205	adantr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) = \{⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)\}$
207	110	adantr	$⊢ (φ \land z \in C) \to K \in TopOn (B)$
208		flfval	$⊢ (K \in TopOn (B) \land nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) = K fLim (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A)$
209	207 190 191 208	syl3anc	$⊢ (φ \land z \in C) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) = K fLim (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A)$
210	209	adantr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) = K fLim (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A)$
211	4	uniexd	$⊢ φ \to ⋃ K \in V$
212	211	ad2antrr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to ⋃ K \in V$
213	2 212	eqeltrid	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to B \in V$
214	190	adantr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A)$
215		filfbas	$⊢ nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A) \to nei (J) (\{z\}) ↾_{𝑡} A \in fBas (A)$
216	214 215	syl	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to nei (J) (\{z\}) ↾_{𝑡} A \in fBas (A)$
217	5	ad2antrr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to F : A ⟶ B$
218		simpr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)$
219		fgfil	$⊢ nei (J) (\{z\}) ↾_{𝑡} A \in Fil (A) \to A filGen (nei (J) (\{z\}) ↾_{𝑡} A) = nei (J) (\{z\}) ↾_{𝑡} A$
220	190 219	syl	$⊢ (φ \land z \in C) \to A filGen (nei (J) (\{z\}) ↾_{𝑡} A) = nei (J) (\{z\}) ↾_{𝑡} A$
221	220	adantr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to A filGen (nei (J) (\{z\}) ↾_{𝑡} A) = nei (J) (\{z\}) ↾_{𝑡} A$
222	218 221	eleqtrrd	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to v \cap A \in (A filGen (nei (J) (\{z\}) ↾_{𝑡} A))$
223		eqid	$⊢ A filGen (nei (J) (\{z\}) ↾_{𝑡} A) = A filGen (nei (J) (\{z\}) ↾_{𝑡} A)$
224	223	imaelfm	$⊢ ((B \in V \land nei (J) (\{z\}) ↾_{𝑡} A \in fBas (A) \land F : A ⟶ B) \land v \cap A \in (A filGen (nei (J) (\{z\}) ↾_{𝑡} A))) \to F [v \cap A] \in (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A)$
225	213 216 217 222 224	syl31anc	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to F [v \cap A] \in (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A)$
226		flimclsi	$⊢ F [v \cap A] \in (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A) \to K fLim (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A) \subseteq cls (K) (F [v \cap A])$
227	225 226	syl	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to K fLim (B FilMap F) (nei (J) (\{z\}) ↾_{𝑡} A) \subseteq cls (K) (F [v \cap A])$
228	210 227	eqsstrd	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \subseteq cls (K) (F [v \cap A])$
229	206 228	eqsstrrd	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to \{⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)\} \subseteq cls (K) (F [v \cap A])$
230		fvex	$⊢ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \in V$
231	230	uniex	$⊢ ⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \in V$
232	231	snss	$⊢ ⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \in cls (K) (F [v \cap A]) \leftrightarrow \{⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F)\} \subseteq cls (K) (F [v \cap A])$
233	229 232	sylibr	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to ⋃ (K fLimf (nei (J) (\{z\}) ↾_{𝑡} A)) (F) \in cls (K) (F [v \cap A])$
234	181 233	eqeltrd	$⊢ ((φ \land z \in C) \land v \cap A \in (nei (J) (\{z\}) ↾_{𝑡} A)) \to (J CnExt K) (F) (z) \in cls (K) (F [v \cap A])$
235	166 172 179 234	syl21anc	$⊢ ((φ \land v \in J) \land z \in v) \to (J CnExt K) (F) (z) \in cls (K) (F [v \cap A])$
236	235	adantlr	$⊢ (((φ \land v \in J) \land cls (K) (F [v \cap A]) \subseteq w) \land z \in v) \to (J CnExt K) (F) (z) \in cls (K) (F [v \cap A])$
237	165 236	sseldd	$⊢ (((φ \land v \in J) \land cls (K) (F [v \cap A]) \subseteq w) \land z \in v) \to (J CnExt K) (F) (z) \in w$
238	237	ralrimiva	$⊢ ((φ \land v \in J) \land cls (K) (F [v \cap A]) \subseteq w) \to \forall z \in v (J CnExt K) (F) (z) \in w$
239	238	expl	$⊢ φ \to ((v \in J \land cls (K) (F [v \cap A]) \subseteq w) \to \forall z \in v (J CnExt K) (F) (z) \in w)$
240	239	reximdv	$⊢ φ \to (\exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w) \to \exists v \in nei (J) (\{x\}) \forall z \in v (J CnExt K) (F) (z) \in w)$
241	240	ad2antrr	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to (\exists v \in nei (J) (\{x\}) (v \in J \land cls (K) (F [v \cap A]) \subseteq w) \to \exists v \in nei (J) (\{x\}) \forall z \in v (J CnExt K) (F) (z) \in w)$
242	164 241	mpd	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists v \in nei (J) (\{x\}) \forall z \in v (J CnExt K) (F) (z) \in w$
243	1 2 3 4 5 6 7 8	cnextf	$⊢ φ \to (J CnExt K) (F) : C ⟶ B$
244	243	ffund	$⊢ φ \to Fun (J CnExt K) (F)$
245	244	adantr	$⊢ (φ \land v \in nei (J) (\{x\})) \to Fun (J CnExt K) (F)$
246	1	neii1	$⊢ (J \in Top \land v \in nei (J) (\{x\})) \to v \subseteq C$
247	3 246	sylan	$⊢ (φ \land v \in nei (J) (\{x\})) \to v \subseteq C$
248	243	fdmd	$⊢ φ \to dom (J CnExt K) (F) = C$
249	248	adantr	$⊢ (φ \land v \in nei (J) (\{x\})) \to dom (J CnExt K) (F) = C$
250	247 249	sseqtrrd	$⊢ (φ \land v \in nei (J) (\{x\})) \to v \subseteq dom (J CnExt K) (F)$
251		funimass4	$⊢ (Fun (J CnExt K) (F) \land v \subseteq dom (J CnExt K) (F)) \to ((J CnExt K) (F) [v] \subseteq w \leftrightarrow \forall z \in v (J CnExt K) (F) (z) \in w)$
252	245 250 251	syl2anc	$⊢ (φ \land v \in nei (J) (\{x\})) \to ((J CnExt K) (F) [v] \subseteq w \leftrightarrow \forall z \in v (J CnExt K) (F) (z) \in w)$
253	252	biimprd	$⊢ (φ \land v \in nei (J) (\{x\})) \to (\forall z \in v (J CnExt K) (F) (z) \in w \to (J CnExt K) (F) [v] \subseteq w)$
254	253	reximdva	$⊢ φ \to (\exists v \in nei (J) (\{x\}) \forall z \in v (J CnExt K) (F) (z) \in w \to \exists v \in nei (J) (\{x\}) (J CnExt K) (F) [v] \subseteq w)$
255	10 242 254	sylc	$⊢ ((φ \land x \in C) \land w \in nei (K) (\{(J CnExt K) (F) (x)\})) \to \exists v \in nei (J) (\{x\}) (J CnExt K) (F) [v] \subseteq w$
256	255	ralrimiva	$⊢ (φ \land x \in C) \to \forall w \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists v \in nei (J) (\{x\}) (J CnExt K) (F) [v] \subseteq w$
257	256	ralrimiva	$⊢ φ \to \forall x \in C \forall w \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists v \in nei (J) (\{x\}) (J CnExt K) (F) [v] \subseteq w$
258	1 2	cnnei	$⊢ (J \in Top \land K \in Top \land (J CnExt K) (F) : C ⟶ B) \to ((J CnExt K) (F) \in (J Cn K) \leftrightarrow \forall x \in C \forall w \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists v \in nei (J) (\{x\}) (J CnExt K) (F) [v] \subseteq w)$
259	3 41 243 258	syl3anc	$⊢ φ \to ((J CnExt K) (F) \in (J Cn K) \leftrightarrow \forall x \in C \forall w \in nei (K) (\{(J CnExt K) (F) (x)\}) \exists v \in nei (J) (\{x\}) (J CnExt K) (F) [v] \subseteq w)$
260	257 259	mpbird	$⊢ φ \to (J CnExt K) (F) \in (J Cn K)$

Metamath Proof Explorer

Theorem cnextcn

Proof