2ndci

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

		Ref	Expression
	Assertion	2ndci	$⊢ (B \in TopBases \land B ≼ ω) \to topGen (B) \in 2^{nd} 𝜔$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (B \in TopBases \land B ≼ ω) \to B \in TopBases$
2		simpr	$⊢ (B \in TopBases \land B ≼ ω) \to B ≼ ω$
3		eqidd	$⊢ (B \in TopBases \land B ≼ ω) \to topGen (B) = topGen (B)$
4		breq1	$⊢ x = B \to (x ≼ ω \leftrightarrow B ≼ ω)$
5		fveqeq2	$⊢ x = B \to (topGen (x) = topGen (B) \leftrightarrow topGen (B) = topGen (B))$
6	4 5	anbi12d	$⊢ x = B \to ((x ≼ ω \land topGen (x) = topGen (B)) \leftrightarrow (B ≼ ω \land topGen (B) = topGen (B)))$
7	6	rspcev	$⊢ (B \in TopBases \land (B ≼ ω \land topGen (B) = topGen (B))) \to \exists x \in TopBases (x ≼ ω \land topGen (x) = topGen (B))$
8	1 2 3 7	syl12anc	$⊢ (B \in TopBases \land B ≼ ω) \to \exists x \in TopBases (x ≼ ω \land topGen (x) = topGen (B))$
9		is2ndc	$⊢ topGen (B) \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = topGen (B))$
10	8 9	sylibr	$⊢ (B \in TopBases \land B ≼ ω) \to topGen (B) \in 2^{nd} 𝜔$

Metamath Proof Explorer