Theorem jumpncnp

Description: Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	jumpncnp.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	jumpncnp.a	$$⊢\phi \to A\subseteq ℝ$$
	jumpncnp.3	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	jumpncnp.f	$$⊢\phi \to F:A⟶ℂ$$
	jumpncnp.b	$$⊢\phi \to B\in ℝ$$
	jumpncnp.lpt1	$$⊢\phi \to B\in \mathrm{limPt}\left(J\right)\left(A\cap \left(\mathrm{-\infty },B\right)\right)$$
	jumpncnp.lpt2	$$⊢\phi \to B\in \mathrm{limPt}\left(J\right)\left(A\cap \left(B,\mathrm{+\infty }\right)\right)$$
	jumpncnp.8	$$⊢\phi \to L\in \left(\left({F\upharpoonright }_{\left(\mathrm{-\infty },B\right)}\right){lim}_{ℂ}B\right)$$
	jumpncnp.9	$$⊢\phi \to R\in \left(\left({F\upharpoonright }_{\left(B,\mathrm{+\infty }\right)}\right){lim}_{ℂ}B\right)$$
	jumpncnp.lner	$$⊢\phi \to L\ne R$$
Assertion	jumpncnp	$$⊢\phi \to \neg F\in \left(J\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		jumpncnp.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		jumpncnp.a	$$⊢\phi \to A\subseteq ℝ$$
3		jumpncnp.3	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4		jumpncnp.f	$$⊢\phi \to F:A⟶ℂ$$
5		jumpncnp.b	$$⊢\phi \to B\in ℝ$$
6		jumpncnp.lpt1	$$⊢\phi \to B\in \mathrm{limPt}\left(J\right)\left(A\cap \left(\mathrm{-\infty },B\right)\right)$$
7		jumpncnp.lpt2	$$⊢\phi \to B\in \mathrm{limPt}\left(J\right)\left(A\cap \left(B,\mathrm{+\infty }\right)\right)$$
8		jumpncnp.8	$$⊢\phi \to L\in \left(\left({F\upharpoonright }_{\left(\mathrm{-\infty },B\right)}\right){lim}_{ℂ}B\right)$$
9		jumpncnp.9	$$⊢\phi \to R\in \left(\left({F\upharpoonright }_{\left(B,\mathrm{+\infty }\right)}\right){lim}_{ℂ}B\right)$$
10		jumpncnp.lner	$$⊢\phi \to L\ne R$$
11	1 2 3 4 6 7 8 9 10	limclner	$$⊢\phi \to F{lim}_{ℂ}B=\varnothing$$
12		ne0i	$$⊢F\left(B\right)\in \left(F{lim}_{ℂ}B\right)\to F{lim}_{ℂ}B\ne \varnothing$$
13	12	necon2bi	$$⊢F{lim}_{ℂ}B=\varnothing \to \neg F\left(B\right)\in \left(F{lim}_{ℂ}B\right)$$
14	11 13	syl	$$⊢\phi \to \neg F\left(B\right)\in \left(F{lim}_{ℂ}B\right)$$
15	14	intnand	$$⊢\phi \to \neg \left(F:ℝ⟶ℂ\wedge F\left(B\right)\in \left(F{lim}_{ℂ}B\right)\right)$$
16		ax-resscn	$$⊢ℝ\subseteq ℂ$$
17		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
18	17	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
19	3 18	eqtri	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
20	17 19	cnplimc	$$⊢\left(ℝ\subseteq ℂ\wedge B\in ℝ\right)\to \left(F\in \left(J\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(B\right)\leftrightarrow \left(F:ℝ⟶ℂ\wedge F\left(B\right)\in \left(F{lim}_{ℂ}B\right)\right)\right)$$
21	16 5 20	sylancr	$$⊢\phi \to \left(F\in \left(J\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(B\right)\leftrightarrow \left(F:ℝ⟶ℂ\wedge F\left(B\right)\in \left(F{lim}_{ℂ}B\right)\right)\right)$$
22	15 21	mtbird	$$⊢\phi \to \neg F\in \left(J\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(B\right)$$