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	$⊢ J \in 2^{nd} 𝜔 \to J \in Top$

Step	Hyp	Ref	Expression
1		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$
2		simprr	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to topGen (x) = J$
3		tgcl	$⊢ x \in TopBases \to topGen (x) \in Top$
4	3	adantr	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to topGen (x) \in Top$
5	2 4	eqeltrrd	$⊢ (x \in TopBases \land (x ≼ ω \land topGen (x) = J)) \to J \in Top$
6	5	rexlimiva	$⊢ \exists x \in TopBases (x ≼ ω \land topGen (x) = J) \to J \in Top$
7	1 6	sylbi	$⊢ J \in 2^{nd} 𝜔 \to J \in Top$

Metamath Proof Explorer