Metamath Proof Explorer


Theorem 2ndci

Description: A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndci ( ( 𝐵 ∈ TopBases ∧ 𝐵 ≼ ω ) → ( topGen ‘ 𝐵 ) ∈ 2ndω )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐵 ∈ TopBases ∧ 𝐵 ≼ ω ) → 𝐵 ∈ TopBases )
2 simpr ( ( 𝐵 ∈ TopBases ∧ 𝐵 ≼ ω ) → 𝐵 ≼ ω )
3 eqidd ( ( 𝐵 ∈ TopBases ∧ 𝐵 ≼ ω ) → ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝐵 ) )
4 breq1 ( 𝑥 = 𝐵 → ( 𝑥 ≼ ω ↔ 𝐵 ≼ ω ) )
5 fveqeq2 ( 𝑥 = 𝐵 → ( ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝐵 ) ↔ ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝐵 ) ) )
6 4 5 anbi12d ( 𝑥 = 𝐵 → ( ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝐵 ) ) ↔ ( 𝐵 ≼ ω ∧ ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝐵 ) ) ) )
7 6 rspcev ( ( 𝐵 ∈ TopBases ∧ ( 𝐵 ≼ ω ∧ ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝐵 ) ) ) → ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝐵 ) ) )
8 1 2 3 7 syl12anc ( ( 𝐵 ∈ TopBases ∧ 𝐵 ≼ ω ) → ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝐵 ) ) )
9 is2ndc ( ( topGen ‘ 𝐵 ) ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝐵 ) ) )
10 8 9 sylibr ( ( 𝐵 ∈ TopBases ∧ 𝐵 ≼ ω ) → ( topGen ‘ 𝐵 ) ∈ 2ndω )