Theorem cnextrel

Description: In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017)

	Ref	Expression
Hypotheses	cnextfrel.1	$$⊢C=\bigcup J$$
	cnextfrel.2	$$⊢B=\bigcup K$$
Assertion	cnextrel	$$⊢\left(\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\wedge \left(F:A⟶B\wedge A\subseteq C\right)\right)\to \mathrm{Rel}\left(J\mathrm{CnExt}K\right)\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnextfrel.1	$$⊢C=\bigcup J$$
2		cnextfrel.2	$$⊢B=\bigcup K$$
3		relxp	$$⊢\mathrm{Rel}\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)$$
4	3	rgenw	$$⊢\forall x\in \mathrm{cls}\left(J\right)\left(A\right)\mathrm{Rel}\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)$$
5		reliun	$$⊢\mathrm{Rel}\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 \forall x\in \mathrm{cls}\left(J\right)\left(A\right)\mathrm{Rel}\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)$$
6	4 5	mpbir	$$⊢\mathrm{Rel}\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)$$
7	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)$$
8	7	releqd	$$⊢\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(\mathrm{Rel}\left(J\mathrm{CnExt}K\right)\left(F\right)\leftrightarrow \mathrm{Rel}\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)$$
9	6 8	mpbiri	$$⊢\left(\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\wedge \left(F:A⟶B\wedge A\subseteq C\right)\right)\to \mathrm{Rel}\left(J\mathrm{CnExt}K\right)\left(F\right)$$