Theorem iccnct

Description: A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021)

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

Proof

Step	Hyp	Ref	Expression
1		iccnct.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		iccnct.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		iccnct.l	$$⊢\phi \to A<B$$
4		iccnct.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		ioossicc	$$⊢\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 }$$