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	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	iccnct.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	iccnct.l	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	iccnct.c	⊢ 𝐶 = ( 𝐴 [,] 𝐵 )
Assertion	iccnct	⊢ ( 𝜑 → ¬ 𝐶 ≼ ω )

Proof

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