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 )