Theorem cnextfres

Description: F and its extension by continuity agree on the domain of F . (Contributed by Thierry Arnoux, 29-Aug-2020)

	Ref	Expression
Hypotheses	cnextfres.c	$$⊢C=\bigcup J$$
	cnextfres.b	$$⊢B=\bigcup K$$
	cnextfres.j	$$⊢\phi \to J\in \mathrm{Top}$$
	cnextfres.k	$$⊢\phi \to K\in \mathrm{Haus}$$
	cnextfres.a	$$⊢\phi \to A\subseteq C$$
	cnextfres.1	$$⊢\phi \to F\in \left(\left(J{\upharpoonright }_{𝑡}A\right)\mathrm{Cn}K\right)$$
	cnextfres.x	$$⊢\phi \to X\in A$$
Assertion	cnextfres	$$⊢\phi \to \left(J\mathrm{CnExt}K\right)\left(F\right)\left(X\right)=F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnextfres.c	$$⊢C=\bigcup J$$
2		cnextfres.b	$$⊢B=\bigcup K$$
3		cnextfres.j	$$⊢\phi \to J\in \mathrm{Top}$$
4		cnextfres.k	$$⊢\phi \to K\in \mathrm{Haus}$$
5		cnextfres.a	$$⊢\phi \to A\subseteq C$$
6		cnextfres.1	$$⊢\phi \to F\in \left(\left(J{\upharpoonright }_{𝑡}A\right)\mathrm{Cn}K\right)$$
7		cnextfres.x	$$⊢\phi \to X\in A$$
8		eqid	$$⊢\bigcup \left(J{\upharpoonright }_{𝑡}A\right)=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
9	8 2	cnf	$$⊢F\in \left(\left(J{\upharpoonright }_{𝑡}A\right)\mathrm{Cn}K\right)\to F:\bigcup \left(J{\upharpoonright }_{𝑡}A\right)⟶B$$
10	6 9	syl	$$⊢\phi \to F:\bigcup \left(J{\upharpoonright }_{𝑡}A\right)⟶B$$
11	1	restuni	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq C\right)\to A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
12	3 5 11	syl2anc	$$⊢\phi \to A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$
13	12	feq2d	$$⊢\phi \to \left(F:A⟶B\leftrightarrow F:\bigcup \left(J{\upharpoonright }_{𝑡}A\right)⟶B\right)$$
14	10 13	mpbird	$$⊢\phi \to F:A⟶B$$
15	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)$$
16	3 4 14 5 15	syl22anc	$$⊢\phi \to \mathrm{Fun}\left(J\mathrm{CnExt}K\right)\left(F\right)$$
17	1	sscls	$$⊢\left(J\in \mathrm{Top}\wedge A\subseteq C\right)\to A\subseteq \mathrm{cls}\left(J\right)\left(A\right)$$
18	3 5 17	syl2anc	$$⊢\phi \to A\subseteq \mathrm{cls}\left(J\right)\left(A\right)$$
19	18 7	sseldd	$$⊢\phi \to X\in \mathrm{cls}\left(J\right)\left(A\right)$$
20	1 2 3 5 6 7	flfcntr	$$⊢\phi \to F\left(X\right)\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right){\upharpoonright }_{𝑡}A\right)\right)\left(F\right)$$
21		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
22	21	fveq2d	$$⊢x=X\to \mathrm{nei}\left(J\right)\left(\left\{x\right\}\right)=\mathrm{nei}\left(J\right)\left(\left\{X\right\}\right)$$
23	22	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$$
24	23	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)$$
25	24	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)$$
26	25	opeliunxp2	$$⊢⟨X,F\left(X\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 F\left(X\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)$$
27	19 20 26	sylanbrc	$$⊢\phi \to ⟨X,F\left(X\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)$$
28		haustop	$$⊢K\in \mathrm{Haus}\to K\in \mathrm{Top}$$
29	4 28	syl	$$⊢\phi \to K\in \mathrm{Top}$$
30	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)$$
31	3 29 14 5 30	syl22anc	$$⊢\phi \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)$$
32	27 31	eleqtrrd	$$⊢\phi \to ⟨X,F\left(X\right)⟩\in \left(J\mathrm{CnExt}K\right)\left(F\right)$$
33		df-br	$$⊢X\left(J\mathrm{CnExt}K\right)\left(F\right)F\left(X\right)\leftrightarrow ⟨X,F\left(X\right)⟩\in \left(J\mathrm{CnExt}K\right)\left(F\right)$$
34	32 33	sylibr	$$⊢\phi \to X\left(J\mathrm{CnExt}K\right)\left(F\right)F\left(X\right)$$
35		funbrfv	$$⊢\mathrm{Fun}\left(J\mathrm{CnExt}K\right)\left(F\right)\to \left(X\left(J\mathrm{CnExt}K\right)\left(F\right)F\left(X\right)\to \left(J\mathrm{CnExt}K\right)\left(F\right)\left(X\right)=F\left(X\right)\right)$$
36	16 34 35	sylc	$$⊢\phi \to \left(J\mathrm{CnExt}K\right)\left(F\right)\left(X\right)=F\left(X\right)$$