Theorem iocnct

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

	Ref	Expression
Hypotheses	iocnct.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	iocnct.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	iocnct.l	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	iocnct.c	⊢ 𝐶 = ( 𝐴 (,] 𝐵 )
Assertion	iocnct	⊢ ( 𝜑 → ¬ 𝐶 ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		iocnct.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		iocnct.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		iocnct.l	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		iocnct.c	⊢ 𝐶 = ( 𝐴 (,] 𝐵 )
5		eqid	⊢ ( 𝐴 (,) 𝐵 ) = ( 𝐴 (,) 𝐵 )
6	1 2 3 5	ioonct	⊢ ( 𝜑 → ¬ ( 𝐴 (,) 𝐵 ) ≼ ω )
7		ioossioc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,] 𝐵 )
8	7 4	sseqtrri	⊢ ( 𝐴 (,) 𝐵 ) ⊆ 𝐶
9	8	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐶 )
10	6 9	ssnct	⊢ ( 𝜑 → ¬ 𝐶 ≼ ω )