Theorem 1stctop

Description: A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009)

	Ref	Expression
Assertion	1stctop	$$⊢J\in 1^{st}𝜔\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	is1stc	$$⊢J\in 1^{st}𝜔\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in \bigcup J\exists y\in 𝒫J\left(y\preccurlyeq \mathrm{\omega }\wedge \forall z\in J\left(x\in z\to x\in \bigcup \left(y\cap 𝒫z\right)\right)\right)\right)$$
3	2	simplbi	$$⊢J\in 1^{st}𝜔\to J\in \mathrm{Top}$$