Metamath Proof Explorer

Theorem met2ndc

Description: A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015)

		Ref	Expression
	Hypothesis	methaus.1	$⊢ J = MetOpen (D)$
	Assertion	met2ndc	$⊢ D \in ∞Met (X) \to (J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X))$

Proof

Step	Hyp	Ref	Expression
1		methaus.1	$⊢ J = MetOpen (D)$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	2ndcsep	$⊢ J \in 2^{nd} 𝜔 \to \exists x \in 𝒫 ⋃ J (x ≼ ω \land cls (J) (x) = ⋃ J)$
4	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
5	4	pweqd	$⊢ D \in ∞Met (X) \to 𝒫 X = 𝒫 ⋃ J$
6	4	eqeq2d	$⊢ D \in ∞Met (X) \to (cls (J) (x) = X \leftrightarrow cls (J) (x) = ⋃ J)$
7	6	anbi2d	$⊢ D \in ∞Met (X) \to ((x ≼ ω \land cls (J) (x) = X) \leftrightarrow (x ≼ ω \land cls (J) (x) = ⋃ J))$
8	5 7	rexeqbidv	$⊢ D \in ∞Met (X) \to (\exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X) \leftrightarrow \exists x \in 𝒫 ⋃ J (x ≼ ω \land cls (J) (x) = ⋃ J))$
9	3 8	syl5ibr	$⊢ D \in ∞Met (X) \to (J \in 2^{nd} 𝜔 \to \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X))$
10		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
11	1	met2ndci	$⊢ (D \in ∞Met (X) \land (x \subseteq X \land x ≼ ω \land cls (J) (x) = X)) \to J \in 2^{nd} 𝜔$
12	11	3exp2	$⊢ D \in ∞Met (X) \to (x \subseteq X \to (x ≼ ω \to (cls (J) (x) = X \to J \in 2^{nd} 𝜔)))$
13	12	imp4a	$⊢ D \in ∞Met (X) \to (x \subseteq X \to ((x ≼ ω \land cls (J) (x) = X) \to J \in 2^{nd} 𝜔))$
14	10 13	syl5	$⊢ D \in ∞Met (X) \to (x \in 𝒫 X \to ((x ≼ ω \land cls (J) (x) = X) \to J \in 2^{nd} 𝜔))$
15	14	rexlimdv	$⊢ D \in ∞Met (X) \to (\exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X) \to J \in 2^{nd} 𝜔)$
16	9 15	impbid	$⊢ D \in ∞Met (X) \to (J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in 𝒫 X (x ≼ ω \land cls (J) (x) = X))$