Theorem iocnct

Description: A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	iocnct.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	iocnct.b	$$⊢\phi \to B\in {ℝ}^{*}$$
	iocnct.l	$$⊢\phi \to A<B$$
	iocnct.c	$$⊢C=\left(A,B\right]$$
Assertion	iocnct	$$⊢\phi \to \neg C\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		iocnct.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		iocnct.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		iocnct.l	$$⊢\phi \to A<B$$
4		iocnct.c	$$⊢C=\left(A,B\right]$$
5		eqid	$$⊢\left(A,B\right)=\left(A,B\right)$$
6	1 2 3 5	ioonct	$$⊢\phi \to \neg \left(A,B\right)\preccurlyeq \mathrm{\omega }$$
7		ioossioc	$$⊢\left(A,B\right)\subseteq \left(A,B\right]$$
8	7 4	sseqtrri	$$⊢\left(A,B\right)\subseteq C$$
9	8	a1i	$$⊢\phi \to \left(A,B\right)\subseteq C$$
10	6 9	ssnct	$$⊢\phi \to \neg C\preccurlyeq \mathrm{\omega }$$