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

Metamath Proof Explorer

Theorem 2ndctop

Description: A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010) (Revised by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndctop ( 𝐽 ∈ 2ndω → 𝐽 ∈ Top )

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )
2 simprr ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( topGen ‘ 𝑥 ) = 𝐽 )
3 tgcl ⊢ ( 𝑥 ∈ TopBases → ( topGen ‘ 𝑥 ) ∈ Top )
4 3 adantr ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( topGen ‘ 𝑥 ) ∈ Top )
5 2 4 eqeltrrd ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → 𝐽 ∈ Top )
6 5 rexlimiva ⊢ ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → 𝐽 ∈ Top )
7 1 6 sylbi ⊢ ( 𝐽 ∈ 2ndω → 𝐽 ∈ Top )