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ω )