Theorem dis1stc

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

	Ref	Expression
Assertion	dis1stc	|- ( X e. V -> ~P X e. 1stc )

Proof

Step	Hyp	Ref	Expression
1		vsnex	|- { x } e. _V
2		distop	|- ( { x } e. _V -> ~P { x } e. Top )
3	1 2	ax-mp	|- ~P { x } e. Top
4		tgtop	|- ( ~P { x } e. Top -> ( topGen ` ~P { x } ) = ~P { x } )
5	3 4	ax-mp	|- ( topGen ` ~P { x } ) = ~P { x }
6		topbas	|- ( ~P { x } e. Top -> ~P { x } e. TopBases )
7	3 6	ax-mp	|- ~P { x } e. TopBases
8		snfi	|- { x } e. Fin
9		pwfi	|- ( { x } e. Fin <-> ~P { x } e. Fin )
10	8 9	mpbi	|- ~P { x } e. Fin
11		isfinite	|- ( ~P { x } e. Fin <-> ~P { x } ~< _om )
12	10 11	mpbi	|- ~P { x } ~< _om
13		sdomdom	|- ( ~P { x } ~< _om -> ~P { x } ~<_ _om )
14	12 13	ax-mp	|- ~P { x } ~<_ _om
15		2ndci	|- ( ( ~P { x } e. TopBases /\ ~P { x } ~<_ _om ) -> ( topGen ` ~P { x } ) e. 2ndc )
16	7 14 15	mp2an	|- ( topGen ` ~P { x } ) e. 2ndc
17	5 16	eqeltrri	|- ~P { x } e. 2ndc
18		2ndc1stc	|- ( ~P { x } e. 2ndc -> ~P { x } e. 1stc )
19	17 18	ax-mp	|- ~P { x } e. 1stc
20	19	rgenw	|- A. x e. X ~P { x } e. 1stc
21		dislly	|- ( X e. V -> ( ~P X e. Locally 1stc <-> A. x e. X ~P { x } e. 1stc ) )
22	20 21	mpbiri	|- ( X e. V -> ~P X e. Locally 1stc )
23		lly1stc	|- Locally 1stc = 1stc
24	22 23	eleqtrdi	|- ( X e. V -> ~P X e. 1stc )