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	$⊢ J \in 2^{nd} 𝜔 \to J ≼ ℝ$

Step	Hyp	Ref	Expression
1		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$
2		tgdom	$⊢ x \in TopBases \to topGen (x) ≼ 𝒫 x$
3		simpr	$⊢ (x \in TopBases \land x ≼ ω) \to x ≼ ω$
4		nnenom	$⊢ ℕ \approx ω$
5	4	ensymi	$⊢ ω \approx ℕ$
6		domentr	$⊢ (x ≼ ω \land ω \approx ℕ) \to x ≼ ℕ$
7	3 5 6	sylancl	$⊢ (x \in TopBases \land x ≼ ω) \to x ≼ ℕ$
8		pwdom	$⊢ x ≼ ℕ \to 𝒫 x ≼ 𝒫 ℕ$
9	7 8	syl	$⊢ (x \in TopBases \land x ≼ ω) \to 𝒫 x ≼ 𝒫 ℕ$
10		rpnnen	$⊢ ℝ \approx 𝒫 ℕ$
11	10	ensymi	$⊢ 𝒫 ℕ \approx ℝ$
12		domentr	$⊢ (𝒫 x ≼ 𝒫 ℕ \land 𝒫 ℕ \approx ℝ) \to 𝒫 x ≼ ℝ$
13	9 11 12	sylancl	$⊢ (x \in TopBases \land x ≼ ω) \to 𝒫 x ≼ ℝ$
14		domtr	$⊢ (topGen (x) ≼ 𝒫 x \land 𝒫 x ≼ ℝ) \to topGen (x) ≼ ℝ$
15	2 13 14	syl2an2r	$⊢ (x \in TopBases \land x ≼ ω) \to topGen (x) ≼ ℝ$
16		breq1	$⊢ topGen (x) = J \to (topGen (x) ≼ ℝ \leftrightarrow J ≼ ℝ)$
17	15 16	syl5ibcom	$⊢ (x \in TopBases \land x ≼ ω) \to (topGen (x) = J \to J ≼ ℝ)$
18	17	expimpd	$⊢ x \in TopBases \to ((x ≼ ω \land topGen (x) = J) \to J ≼ ℝ)$
19	18	rexlimiv	$⊢ \exists x \in TopBases (x ≼ ω \land topGen (x) = J) \to J ≼ ℝ$
20	1 19	sylbi	$⊢ J \in 2^{nd} 𝜔 \to J ≼ ℝ$

Metamath Proof Explorer