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	|- ( ph -> A e. RR* )
	iccnct.b	|- ( ph -> B e. RR* )
	iccnct.l	|- ( ph -> A < B )
	iccnct.c	|- C = ( A [,] B )
Assertion	iccnct	|- ( ph -> -. C ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		iccnct.a	|- ( ph -> A e. RR* )
2		iccnct.b	|- ( ph -> B e. RR* )
3		iccnct.l	|- ( ph -> A < B )
4		iccnct.c	|- C = ( A [,] B )
5		eqid	|- ( A (,) B ) = ( A (,) B )
6	1 2 3 5	ioonct	|- ( ph -> -. ( A (,) B ) ~<_ _om )
7		ioossicc	|- ( A (,) B ) C_ ( A [,] B )
8	7 4	sseqtrri	|- ( A (,) B ) C_ C
9	8	a1i	|- ( ph -> ( A (,) B ) C_ C )
10	6 9	ssnct	|- ( ph -> -. C ~<_ _om )