Metamath Proof Explorer

Theorem rectbntr0

Description: A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Assertion rectbntr0 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 nnex ⊢ ℕ ∈ V
2 1 canth2 ⊢ ℕ ≺ 𝒫 ℕ
3 domnsym ⊢ ( 𝒫 ℕ ≼ ℕ → ¬ ℕ ≺ 𝒫 ℕ )
4 2 3 mt2 ⊢ ¬ 𝒫 ℕ ≼ ℕ
5 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
6 simpl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → 𝐴 ⊆ ℝ )
7 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
8 7 ntropn ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐴 ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ∈ ( topGen ‘ ran (,) ) )
9 5 6 8 sylancr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ∈ ( topGen ‘ ran (,) ) )
10 opnreen ⊢ ( ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ∈ ( topGen ‘ ran (,) ) ∧ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≠ ∅ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≈ 𝒫 ℕ )
11 10 ex ⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ∈ ( topGen ‘ ran (,) ) → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≠ ∅ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≈ 𝒫 ℕ ) )
12 9 11 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≠ ∅ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≈ 𝒫 ℕ ) )
13 reex ⊢ ℝ ∈ V
14 13 ssex ⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
15 7 ntrss2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐴 ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ⊆ 𝐴 )
16 5 15 mpan ⊢ ( 𝐴 ⊆ ℝ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ⊆ 𝐴 )
17 ssdomg ⊢ ( 𝐴 ∈ V → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ⊆ 𝐴 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ 𝐴 ) )
18 14 16 17 sylc ⊢ ( 𝐴 ⊆ ℝ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ 𝐴 )
19 domtr ⊢ ( ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ 𝐴 ∧ 𝐴 ≼ ℕ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ ℕ )
20 18 19 sylan ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ ℕ )
21 ensym ⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≈ 𝒫 ℕ → 𝒫 ℕ ≈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) )
22 endomtr ⊢ ( ( 𝒫 ℕ ≈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ∧ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ ℕ ) → 𝒫 ℕ ≼ ℕ )
23 22 expcom ⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≼ ℕ → ( 𝒫 ℕ ≈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) → 𝒫 ℕ ≼ ℕ ) )
24 20 21 23 syl2im ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≈ 𝒫 ℕ → 𝒫 ℕ ≼ ℕ ) )
25 12 24 syld ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ≠ ∅ → 𝒫 ℕ ≼ ℕ ) )
26 25 necon1bd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ¬ 𝒫 ℕ ≼ ℕ → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = ∅ ) )
27 4 26 mpi ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = ∅ )