Theorem dis1stc

Description: A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	dis1stc	$$⊢X\in V\to 𝒫X\in 1^{st}𝜔$$

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
2		distop	$$⊢\left\{x\right\}\in \mathrm{V}\to 𝒫\left\{x\right\}\in \mathrm{Top}$$
3	1 2	ax-mp	$$⊢𝒫\left\{x\right\}\in \mathrm{Top}$$
4		tgtop	$$⊢𝒫\left\{x\right\}\in \mathrm{Top}\to \mathrm{topGen}\left(𝒫\left\{x\right\}\right)=𝒫\left\{x\right\}$$
5	3 4	ax-mp	$$⊢\mathrm{topGen}\left(𝒫\left\{x\right\}\right)=𝒫\left\{x\right\}$$
6		topbas	$$⊢𝒫\left\{x\right\}\in \mathrm{Top}\to 𝒫\left\{x\right\}\in \mathrm{TopBases}$$
7	3 6	ax-mp	$$⊢𝒫\left\{x\right\}\in \mathrm{TopBases}$$
8		snfi	$$⊢\left\{x\right\}\in \mathrm{Fin}$$
9		pwfi	$$⊢\left\{x\right\}\in \mathrm{Fin}\leftrightarrow 𝒫\left\{x\right\}\in \mathrm{Fin}$$
10	8 9	mpbi	$$⊢𝒫\left\{x\right\}\in \mathrm{Fin}$$
11		isfinite	$$⊢𝒫\left\{x\right\}\in \mathrm{Fin}\leftrightarrow 𝒫\left\{x\right\}\prec \mathrm{\omega }$$
12	10 11	mpbi	$$⊢𝒫\left\{x\right\}\prec \mathrm{\omega }$$
13		sdomdom	$$⊢𝒫\left\{x\right\}\prec \mathrm{\omega }\to 𝒫\left\{x\right\}\preccurlyeq \mathrm{\omega }$$
14	12 13	ax-mp	$$⊢𝒫\left\{x\right\}\preccurlyeq \mathrm{\omega }$$
15		2ndci	$$⊢\left(𝒫\left\{x\right\}\in \mathrm{TopBases}\wedge 𝒫\left\{x\right\}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{topGen}\left(𝒫\left\{x\right\}\right)\in 2^{nd}𝜔$$
16	7 14 15	mp2an	$$⊢\mathrm{topGen}\left(𝒫\left\{x\right\}\right)\in 2^{nd}𝜔$$
17	5 16	eqeltrri	$$⊢𝒫\left\{x\right\}\in 2^{nd}𝜔$$
18		2ndc1stc	$$⊢𝒫\left\{x\right\}\in 2^{nd}𝜔\to 𝒫\left\{x\right\}\in 1^{st}𝜔$$
19	17 18	ax-mp	$$⊢𝒫\left\{x\right\}\in 1^{st}𝜔$$
20	19	rgenw	$$⊢\forall x\in X𝒫\left\{x\right\}\in 1^{st}𝜔$$
21		dislly
22	20 21	mpbiri
23		lly1stc
24	22 23	eleqtrdi	$$⊢X\in V\to 𝒫X\in 1^{st}𝜔$$