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

Metamath Proof Explorer

Theorem 2ndcredom

Description: A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion 2ndcredom ( 𝐽 ∈ 2ndω → 𝐽 ≼ ℝ )

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )
2 tgdom ⊢ ( 𝑥 ∈ TopBases → ( topGen ‘ 𝑥 ) ≼ 𝒫 𝑥 )
3 simpr ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝑥 ≼ ω ) → 𝑥 ≼ ω )
4 nnenom ⊢ ℕ ≈ ω
5 4 ensymi ⊢ ω ≈ ℕ
6 domentr ⊢ ( ( 𝑥 ≼ ω ∧ ω ≈ ℕ ) → 𝑥 ≼ ℕ )
7 3 5 6 sylancl ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝑥 ≼ ω ) → 𝑥 ≼ ℕ )
8 pwdom ⊢ ( 𝑥 ≼ ℕ → 𝒫 𝑥 ≼ 𝒫 ℕ )
9 7 8 syl ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝑥 ≼ ω ) → 𝒫 𝑥 ≼ 𝒫 ℕ )
10 rpnnen ⊢ ℝ ≈ 𝒫 ℕ
11 10 ensymi ⊢ 𝒫 ℕ ≈ ℝ
12 domentr ⊢ ( ( 𝒫 𝑥 ≼ 𝒫 ℕ ∧ 𝒫 ℕ ≈ ℝ ) → 𝒫 𝑥 ≼ ℝ )
13 9 11 12 sylancl ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝑥 ≼ ω ) → 𝒫 𝑥 ≼ ℝ )
14 domtr ⊢ ( ( ( topGen ‘ 𝑥 ) ≼ 𝒫 𝑥 ∧ 𝒫 𝑥 ≼ ℝ ) → ( topGen ‘ 𝑥 ) ≼ ℝ )
15 2 13 14 syl2an2r ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝑥 ≼ ω ) → ( topGen ‘ 𝑥 ) ≼ ℝ )
16 breq1 ⊢ ( ( topGen ‘ 𝑥 ) = 𝐽 → ( ( topGen ‘ 𝑥 ) ≼ ℝ ↔ 𝐽 ≼ ℝ ) )
17 15 16 syl5ibcom ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝑥 ≼ ω ) → ( ( topGen ‘ 𝑥 ) = 𝐽 → 𝐽 ≼ ℝ ) )
18 17 expimpd ⊢ ( 𝑥 ∈ TopBases → ( ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → 𝐽 ≼ ℝ ) )
19 18 rexlimiv ⊢ ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → 𝐽 ≼ ℝ )
20 1 19 sylbi ⊢ ( 𝐽 ∈ 2ndω → 𝐽 ≼ ℝ )