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

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 ⊢ 𝐽 = ( 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 imbitrrid ⊢ ( 𝐷 ∈ ( ∞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 ‘ 𝐽 ) ‘ 𝑥 ) = 𝑋 ) ) )