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