This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ¬ 𝐶 ≼ ω )