Theorem iocnct

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

	Ref	Expression
Hypotheses	iocnct.a	|- ( ph -> A e. RR* )
	iocnct.b	|- ( ph -> B e. RR* )
	iocnct.l	|- ( ph -> A < B )
	iocnct.c	|- C = ( A (,] B )
Assertion	iocnct	|- ( ph -> -. C ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		iocnct.a	|- ( ph -> A e. RR* )
2		iocnct.b	|- ( ph -> B e. RR* )
3		iocnct.l	|- ( ph -> A < B )
4		iocnct.c	|- C = ( A (,] B )
5		eqid	|- ( A (,) B ) = ( A (,) B )
6	1 2 3 5	ioonct	|- ( ph -> -. ( A (,) B ) ~<_ _om )
7		ioossioc	|- ( 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 )