This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )