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ω → 𝐽 ≼ ℝ )