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	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	met2ndc	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		methaus.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	2ndcsep	⊢ ( 𝐽 ∈ 2ndω → ∃ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ∪ 𝐽 ) )
4	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
5	4	pweqd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝒫 𝑋 = 𝒫 ∪ 𝐽 )
6	4	eqeq2d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ∪ 𝐽 ) )
7	6	anbi2d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ↔ ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ∪ 𝐽 ) ) )
8	5 7	rexeqbidv	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ↔ ∃ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ∪ 𝐽 ) ) )
9	3 8	syl5ibr	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐽 ∈ 2ndω → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )
10		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
11	1	met2ndci	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) → 𝐽 ∈ 2ndω )
12	11	3exp2	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 → ( 𝑥 ≼ ω → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 → 𝐽 ∈ 2ndω ) ) ) )
13	12	imp4a	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 → ( ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) → 𝐽 ∈ 2ndω ) ) )
14	10 13	syl5	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝒫 𝑋 → ( ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) → 𝐽 ∈ 2ndω ) ) )
15	14	rexlimdv	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) → 𝐽 ∈ 2ndω ) )
16	9 15	impbid	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )