Metamath Proof Explorer

Theorem opnreen

Description: Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 20-Feb-2015)

Ref Expression
Assertion opnreen ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≈ 𝒫 ℕ )

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 elssuni ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ⊆ ∪ ( topGen ‘ ran (,) ) )
3 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
4 2 3 sseqtrrdi ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ⊆ ℝ )
5 ssdomg ⊢ ( ℝ ∈ V → ( 𝐴 ⊆ ℝ → 𝐴 ≼ ℝ ) )
6 1 4 5 mpsyl ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ≼ ℝ )
7 rpnnen ⊢ ℝ ≈ 𝒫 ℕ
8 domentr ⊢ ( ( 𝐴 ≼ ℝ ∧ ℝ ≈ 𝒫 ℕ ) → 𝐴 ≼ 𝒫 ℕ )
9 6 7 8 sylancl ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ≼ 𝒫 ℕ )
10 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
11 4 sselda ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
12 rpnnen2 ⊢ 𝒫 ℕ ≼ ( 0 [,] 1 )
13 rphalfcl ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
14 13 rpred ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
15 resubcl ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) → ( 𝑥 − ( 𝑦 / 2 ) ) ∈ ℝ )
16 14 15 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − ( 𝑦 / 2 ) ) ∈ ℝ )
17 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) → ( 𝑥 + ( 𝑦 / 2 ) ) ∈ ℝ )
18 14 17 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 + ( 𝑦 / 2 ) ) ∈ ℝ )
19 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
20 ltsubrp ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → ( 𝑥 − ( 𝑦 / 2 ) ) < 𝑥 )
21 13 20 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − ( 𝑦 / 2 ) ) < 𝑥 )
22 ltaddrp ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → 𝑥 < ( 𝑥 + ( 𝑦 / 2 ) ) )
23 13 22 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝑥 < ( 𝑥 + ( 𝑦 / 2 ) ) )
24 16 19 18 21 23 lttrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − ( 𝑦 / 2 ) ) < ( 𝑥 + ( 𝑦 / 2 ) ) )
25 iccen ⊢ ( ( ( 𝑥 − ( 𝑦 / 2 ) ) ∈ ℝ ∧ ( 𝑥 + ( 𝑦 / 2 ) ) ∈ ℝ ∧ ( 𝑥 − ( 𝑦 / 2 ) ) < ( 𝑥 + ( 𝑦 / 2 ) ) ) → ( 0 [,] 1 ) ≈ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) )
26 16 18 24 25 syl3anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 0 [,] 1 ) ≈ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) )
27 domentr ⊢ ( ( 𝒫 ℕ ≼ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ≈ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ) → 𝒫 ℕ ≼ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) )
28 12 26 27 sylancr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝒫 ℕ ≼ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) )
29 ovex ⊢ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ∈ V
30 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
31 resubcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 − 𝑦 ) ∈ ℝ )
32 30 31 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − 𝑦 ) ∈ ℝ )
33 32 rexrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − 𝑦 ) ∈ ℝ* )
34 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
35 30 34 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
36 35 rexrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
37 19 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
38 14 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ )
39 38 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℂ )
40 37 39 39 subsub4d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) − ( 𝑦 / 2 ) ) = ( 𝑥 − ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
41 30 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ )
42 41 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℂ )
43 42 2halvesd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
44 43 oveq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( 𝑥 − 𝑦 ) )
45 40 44 eqtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) − ( 𝑦 / 2 ) ) = ( 𝑥 − 𝑦 ) )
46 13 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 2 ) ∈ ℝ+ )
47 16 46 ltsubrpd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) − ( 𝑦 / 2 ) ) < ( 𝑥 − ( 𝑦 / 2 ) ) )
48 45 47 eqbrtrrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 − 𝑦 ) < ( 𝑥 − ( 𝑦 / 2 ) ) )
49 18 46 ltaddrpd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 + ( 𝑦 / 2 ) ) < ( ( 𝑥 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) )
50 37 39 39 addassd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝑥 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
51 43 oveq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 + ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) = ( 𝑥 + 𝑦 ) )
52 50 51 eqtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 + ( 𝑦 / 2 ) ) + ( 𝑦 / 2 ) ) = ( 𝑥 + 𝑦 ) )
53 49 52 breqtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 + ( 𝑦 / 2 ) ) < ( 𝑥 + 𝑦 ) )
54 iccssioo ⊢ ( ( ( ( 𝑥 − 𝑦 ) ∈ ℝ* ∧ ( 𝑥 + 𝑦 ) ∈ ℝ* ) ∧ ( ( 𝑥 − 𝑦 ) < ( 𝑥 − ( 𝑦 / 2 ) ) ∧ ( 𝑥 + ( 𝑦 / 2 ) ) < ( 𝑥 + 𝑦 ) ) ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ⊆ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
55 33 36 48 53 54 syl22anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ⊆ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
56 ssdomg ⊢ ( ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ∈ V → ( ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ⊆ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ≼ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ) )
57 29 55 56 mpsyl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ≼ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
58 domtr ⊢ ( ( 𝒫 ℕ ≼ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ∧ ( ( 𝑥 − ( 𝑦 / 2 ) ) [,] ( 𝑥 + ( 𝑦 / 2 ) ) ) ≼ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ) → 𝒫 ℕ ≼ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
59 28 57 58 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝒫 ℕ ≼ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
60 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
61 60 bl2ioo ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) = ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
62 30 61 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) = ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
63 59 62 breqtrrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → 𝒫 ℕ ≼ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) )
64 11 63 sylan ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → 𝒫 ℕ ≼ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) )
65 simplll ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) → 𝐴 ∈ ( topGen ‘ ran (,) ) )
66 simpr ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 )
67 ssdomg ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ≼ 𝐴 ) )
68 65 66 67 sylc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ≼ 𝐴 )
69 domtr ⊢ ( ( 𝒫 ℕ ≼ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ≼ 𝐴 ) → 𝒫 ℕ ≼ 𝐴 )
70 64 68 69 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) → 𝒫 ℕ ≼ 𝐴 )
71 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
72 60 71 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
73 72 eleq2i ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ 𝐴 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) )
74 60 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
75 71 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐴 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 )
76 74 75 mp3an1 ⊢ ( ( 𝐴 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 )
77 73 76 sylanb ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 )
78 70 77 r19.29a ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ℕ ≼ 𝐴 )
79 78 ex ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( 𝑥 ∈ 𝐴 → 𝒫 ℕ ≼ 𝐴 ) )
80 79 exlimdv ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝒫 ℕ ≼ 𝐴 ) )
81 10 80 syl5bi ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( 𝐴 ≠ ∅ → 𝒫 ℕ ≼ 𝐴 ) )
82 81 imp ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → 𝒫 ℕ ≼ 𝐴 )
83 sbth ⊢ ( ( 𝐴 ≼ 𝒫 ℕ ∧ 𝒫 ℕ ≼ 𝐴 ) → 𝐴 ≈ 𝒫 ℕ )
84 9 82 83 syl2an2r ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≈ 𝒫 ℕ )