Metamath Proof Explorer

Theorem ioonct

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

Ref Expression
Hypotheses ioonct.b ⊢ φ → A ∈ ℝ *
ioonct.c ⊢ φ → B ∈ ℝ *
ioonct.l ⊢ φ → A < B
ioonct.a ⊢ C = A B
Assertion ioonct ⊢ φ → ¬ C ≼ ω

Proof

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