Theorem ioonct

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

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

Proof

Step	Hyp	Ref	Expression
1		ioonct.b	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		ioonct.c	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		ioonct.l	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		ioonct.a	⊢ 𝐶 = ( 𝐴 (,) 𝐵 )
5		ioontr	⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )
6	5	a1i	⊢ ( ( 𝜑 ∧ 𝐶 ≼ ω ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
7		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
8	7	a1i	⊢ ( ( 𝜑 ∧ 𝐶 ≼ ω ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
9	4	breq1i	⊢ ( 𝐶 ≼ ω ↔ ( 𝐴 (,) 𝐵 ) ≼ ω )
10	9	biimpi	⊢ ( 𝐶 ≼ ω → ( 𝐴 (,) 𝐵 ) ≼ ω )
11		nnenom	⊢ ℕ ≈ ω
12	11	ensymi	⊢ ω ≈ ℕ
13	12	a1i	⊢ ( 𝐶 ≼ ω → ω ≈ ℕ )
14		domentr	⊢ ( ( ( 𝐴 (,) 𝐵 ) ≼ ω ∧ ω ≈ ℕ ) → ( 𝐴 (,) 𝐵 ) ≼ ℕ )
15	10 13 14	syl2anc	⊢ ( 𝐶 ≼ ω → ( 𝐴 (,) 𝐵 ) ≼ ℕ )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝐶 ≼ ω ) → ( 𝐴 (,) 𝐵 ) ≼ ℕ )
17		rectbntr0	⊢ ( ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ ∧ ( 𝐴 (,) 𝐵 ) ≼ ℕ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ∅ )
18	8 16 17	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 ≼ ω ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ∅ )
19	6 18	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐶 ≼ ω ) → ( 𝐴 (,) 𝐵 ) = ∅ )
20		ioon0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ 𝐴 < 𝐵 ) )
21	1 2 20	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ 𝐴 < 𝐵 ) )
22	3 21	mpbird	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
23	22	neneqd	⊢ ( 𝜑 → ¬ ( 𝐴 (,) 𝐵 ) = ∅ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≼ ω ) → ¬ ( 𝐴 (,) 𝐵 ) = ∅ )
25	19 24	pm2.65da	⊢ ( 𝜑 → ¬ 𝐶 ≼ ω )