Theorem cnextfvval

Description: The value of the continuous extension of a given function F at a point X . (Contributed by Thierry Arnoux, 21-Dec-2017)

	Ref	Expression
Hypotheses	cnextf.1	$$⊢C=\bigcup J$$
	cnextf.2	$$⊢B=\bigcup K$$
	cnextf.3	$$⊢\phi \to J\in \mathrm{Top}$$
	cnextf.4	$$⊢\phi \to K\in \mathrm{Haus}$$
	cnextf.5	$$⊢\phi \to F:A⟶B$$
	cnextf.a	$$⊢\phi \to A\subseteq C$$
	cnextf.6	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(A\right)=C$$
	cnextf.7	$$⊢\left(\phi \wedge x\in C\right)\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\ne \varnothing$$
Assertion	cnextfvval	$$⊢\left(\phi \wedge X\in C\right)\to \left(J\mathrm{CnExt}K\right)\left(F\right)\left(X\right)=\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnextf.1	$$⊢C=\bigcup J$$
2		cnextf.2	$$⊢B=\bigcup K$$
3		cnextf.3	$$⊢\phi \to J\in \mathrm{Top}$$
4		cnextf.4	$$⊢\phi \to K\in \mathrm{Haus}$$
5		cnextf.5	$$⊢\phi \to F:A⟶B$$
6		cnextf.a	$$⊢\phi \to A\subseteq C$$
7		cnextf.6	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(A\right)=C$$
8		cnextf.7	$$⊢\left(\phi \wedge x\in C\right)\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\ne \varnothing$$
9	3	adantr	$$⊢\left(\phi \wedge X\in C\right)\to J\in \mathrm{Top}$$
10	4	adantr	$$⊢\left(\phi \wedge X\in C\right)\to K\in \mathrm{Haus}$$
11	5	adantr	$$⊢\left(\phi \wedge X\in C\right)\to F:A⟶B$$
12	6	adantr	$$⊢\left(\phi \wedge X\in C\right)\to A\subseteq C$$
13	1 2	cnextfun	$$⊢\left(\left(J\in \mathrm{Top}\wedge K\in \mathrm{Haus}\right)\wedge \left(F:A⟶B\wedge A\subseteq C\right)\right)\to \mathrm{Fun}\left(J\mathrm{CnExt}K\right)\left(F\right)$$
14	9 10 11 12 13	syl22anc	$$⊢\left(\phi \wedge X\in C\right)\to \mathrm{Fun}\left(J\mathrm{CnExt}K\right)\left(F\right)$$
15	7	eleq2d	$$⊢\phi \to \left(X\in \mathrm{cls}\left(J\right)\left(A\right)\leftrightarrow X\in C\right)$$
16	15	biimpar	$$⊢\left(\phi \wedge X\in C\right)\to X\in \mathrm{cls}\left(J\right)\left(A\right)$$
17		fvex	$$⊢\left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \mathrm{V}$$
18	17	uniex	$$⊢\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \mathrm{V}$$
19	18	snid	$$⊢\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left\{\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right\}$$
20		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
21	20	fveq2d	$$⊢x=X\to \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right)=\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right)$$
22	21	oveq1d	$$⊢x=X\to \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A=\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A$$
23	22	oveq2d	$$⊢x=X\to K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)=K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)$$
24	23	fveq1d	$$⊢x=X\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)=\left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)$$
25	24	breq1d	$$⊢x=X\to \left(\left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\leftrightarrow \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\right)$$
26	25	imbi2d	$$⊢x=X\to \left(\left(\phi \to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\right)\leftrightarrow \left(\phi \to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\right)\right)$$
27	4	adantr	$$⊢\left(\phi \wedge x\in C\right)\to K\in \mathrm{Haus}$$
28	3	adantr	$$⊢\left(\phi \wedge x\in C\right)\to J\in \mathrm{Top}$$
29	1	toptopon	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(C\right)$$
30	28 29	sylib	$$⊢\left(\phi \wedge x\in C\right)\to J\in \mathrm{TopOn}\left(C\right)$$
31	6	adantr	$$⊢\left(\phi \wedge x\in C\right)\to A\subseteq C$$
32		simpr	$$⊢\left(\phi \wedge x\in C\right)\to x\in C$$
33	7	eleq2d	$$⊢\phi \to \left(x\in \mathrm{cls}\left(J\right)\left(A\right)\leftrightarrow x\in C\right)$$
34	33	biimpar	$$⊢\left(\phi \wedge x\in C\right)\to x\in \mathrm{cls}\left(J\right)\left(A\right)$$
35		trnei	$$⊢\left(J\in \mathrm{TopOn}\left(C\right)\wedge A\subseteq C\wedge x\in C\right)\to \left(x\in \mathrm{cls}\left(J\right)\left(A\right)\leftrightarrow \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\in \mathrm{Fil}\left(A\right)\right)$$
36	35	biimpa	$$⊢\left(\left(J\in \mathrm{TopOn}\left(C\right)\wedge A\subseteq C\wedge x\in C\right)\wedge x\in \mathrm{cls}\left(J\right)\left(A\right)\right)\to \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\in \mathrm{Fil}\left(A\right)$$
37	30 31 32 34 36	syl31anc	$$⊢\left(\phi \wedge x\in C\right)\to \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\in \mathrm{Fil}\left(A\right)$$
38	5	adantr	$$⊢\left(\phi \wedge x\in C\right)\to F:A⟶B$$
39	2	hausflf2	$$⊢\left(\left(K\in \mathrm{Haus}\wedge \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\in \mathrm{Fil}\left(A\right)\wedge F:A⟶B\right)\wedge \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\ne \varnothing \right)\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}$$
40	27 37 38 8 39	syl31anc	$$⊢\left(\phi \wedge x\in C\right)\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}$$
41	40	expcom	$$⊢x\in C\to \left(\phi \to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\right)$$
42	26 41	vtoclga	$$⊢X\in C\to \left(\phi \to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\right)$$
43	42	impcom	$$⊢\left(\phi \wedge X\in C\right)\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}$$
44		en1b	$$⊢\left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\approx 1_{𝑜}\leftrightarrow \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)=\left\{\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right\}$$
45	43 44	sylib	$$⊢\left(\phi \wedge X\in C\right)\to \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)=\left\{\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right\}$$
46	19 45	eleqtrrid	$$⊢\left(\phi \wedge X\in C\right)\to \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)$$
47		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
48	47	nfel2	$$⊢Ⅎx⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
49		nfv	$$⊢Ⅎx\left(X\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
50	48 49	nfbi	$$⊢Ⅎx\left(⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(X\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
51		opeq1	$$⊢x=X\to ⟨x,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩=⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩$$
52	51	eleq1d	$$⊢x=X\to \left(⟨x,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow ⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
53		eleq1	$$⊢x=X\to \left(x\in \mathrm{cls}\left(J\right)\left(A\right)\leftrightarrow X\in \mathrm{cls}\left(J\right)\left(A\right)\right)$$
54	24	eleq2d	$$⊢x=X\to \left(\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\leftrightarrow \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
55	53 54	anbi12d	$$⊢x=X\to \left(\left(x\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(X\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
56	52 55	bibi12d	$$⊢x=X\to \left(\left(⟨x,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(x\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)\leftrightarrow \left(⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(X\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)\right)$$
57		opeliunxp	$$⊢⟨x,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(x\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
58	50 56 57	vtoclg1f	$$⊢X\in C\to \left(⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(X\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
59	58	adantl	$$⊢\left(\phi \wedge X\in C\right)\to \left(⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\leftrightarrow \left(X\in \mathrm{cls}\left(J\right)\left(A\right)\wedge \bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
60	16 46 59	mpbir2and	$$⊢\left(\phi \wedge X\in C\right)\to ⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
61		df-br	$$⊢X\left(J\mathrm{CnExt}K\right)\left(F\right)\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\leftrightarrow ⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \left(J\mathrm{CnExt}K\right)\left(F\right)$$
62		haustop	$$⊢K\in \mathrm{Haus}\to K\in \mathrm{Top}$$
63	4 62	syl	$$⊢\phi \to K\in \mathrm{Top}$$
64	63	adantr	$$⊢\left(\phi \wedge X\in C\right)\to K\in \mathrm{Top}$$
65	1 2	cnextfval	$$⊢\left(\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\wedge \left(F:A⟶B\wedge A\subseteq C\right)\right)\to \left(J\mathrm{CnExt}K\right)\left(F\right)=\bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
66	9 64 11 12 65	syl22anc	$$⊢\left(\phi \wedge X\in C\right)\to \left(J\mathrm{CnExt}K\right)\left(F\right)=\bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
67	66	eleq2d	$$⊢\left(\phi \wedge X\in C\right)\to \left(⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \left(J\mathrm{CnExt}K\right)\left(F\right)\leftrightarrow ⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
68	61 67	bitrid	$$⊢\left(\phi \wedge X\in C\right)\to \left(X\left(J\mathrm{CnExt}K\right)\left(F\right)\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\leftrightarrow ⟨X,\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)⟩\in \bigcup _{x\in \mathrm{cls}\left(J\right)\left(A\right)}\left(\left\{x\right\}\times \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{x\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)\right)$$
69	60 68	mpbird	$$⊢\left(\phi \wedge X\in C\right)\to X\left(J\mathrm{CnExt}K\right)\left(F\right)\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)$$
70		funbrfv	$$⊢\mathrm{Fun}\left(J\mathrm{CnExt}K\right)\left(F\right)\to \left(X\left(J\mathrm{CnExt}K\right)\left(F\right)\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\to \left(J\mathrm{CnExt}K\right)\left(F\right)\left(X\right)=\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)\right)$$
71	14 69 70	sylc	$$⊢\left(\phi \wedge X\in C\right)\to \left(J\mathrm{CnExt}K\right)\left(F\right)\left(X\right)=\bigcup \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)$$