Metamath Proof Explorer

Theorem dis2ndc

Description: A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Assertion dis2ndc 
|- ( X ~<_ _om <-> ~P X e. 2ndc )

Proof

Step Hyp Ref Expression
1 ctex 
 |-  ( X ~<_ _om -> X e. _V )
2 pwexr 
 |-  ( ~P X e. 2ndc -> X e. _V )
3 vsnex 
 |-  { x } e. _V
4 3 2a1i 
 |-  ( X e. _V -> ( x e. X -> { x } e. _V ) )
5 vex 
 |-  x e. _V
6 5 sneqr 
 |-  ( { x } = { y } -> x = y )
7 sneq 
 |-  ( x = y -> { x } = { y } )
8 6 7 impbii 
 |-  ( { x } = { y } <-> x = y )
9 8 2a1i 
 |-  ( X e. _V -> ( ( x e. X /\ y e. X ) -> ( { x } = { y } <-> x = y ) ) )
10 4 9 dom2lem 
 |-  ( X e. _V -> ( x e. X |-> { x } ) : X -1-1-> _V )
11 f1f1orn 
 |-  ( ( x e. X |-> { x } ) : X -1-1-> _V -> ( x e. X |-> { x } ) : X -1-1-onto-> ran ( x e. X |-> { x } ) )
12 10 11 syl 
 |-  ( X e. _V -> ( x e. X |-> { x } ) : X -1-1-onto-> ran ( x e. X |-> { x } ) )
13 f1oeng 
 |-  ( ( X e. _V /\ ( x e. X |-> { x } ) : X -1-1-onto-> ran ( x e. X |-> { x } ) ) -> X ~~ ran ( x e. X |-> { x } ) )
14 12 13 mpdan 
 |-  ( X e. _V -> X ~~ ran ( x e. X |-> { x } ) )
15 domen1 
 |-  ( X ~~ ran ( x e. X |-> { x } ) -> ( X ~<_ _om <-> ran ( x e. X |-> { x } ) ~<_ _om ) )
16 14 15 syl 
 |-  ( X e. _V -> ( X ~<_ _om <-> ran ( x e. X |-> { x } ) ~<_ _om ) )
17 distop 
 |-  ( X e. _V -> ~P X e. Top )
18 5 snelpw 
 |-  ( x e. X <-> { x } e. ~P X )
19 18 bilani 
 |-  ( ( X e. _V /\ x e. X ) -> { x } e. ~P X )
20 19 fmpttd 
 |-  ( X e. _V -> ( x e. X |-> { x } ) : X --> ~P X )
21 20 frnd 
 |-  ( X e. _V -> ran ( x e. X |-> { x } ) C_ ~P X )
22 elpwi 
 |-  ( y e. ~P X -> y C_ X )
23 22 ad2antrl 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> y C_ X )
24 simprr 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. y )
25 23 24 sseldd 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. X )
26 eqidd 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } = { z } )
27 sneq 
 |-  ( x = z -> { x } = { z } )
28 27 rspceeqv 
 |-  ( ( z e. X /\ { z } = { z } ) -> E. x e. X { z } = { x } )
29 25 26 28 syl2anc 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> E. x e. X { z } = { x } )
30 vsnex 
 |-  { z } e. _V
31 eqid 
 |-  ( x e. X |-> { x } ) = ( x e. X |-> { x } )
32 31 elrnmpt 
 |-  ( { z } e. _V -> ( { z } e. ran ( x e. X |-> { x } ) <-> E. x e. X { z } = { x } ) )
33 30 32 ax-mp 
 |-  ( { z } e. ran ( x e. X |-> { x } ) <-> E. x e. X { z } = { x } )
34 29 33 sylibr 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } e. ran ( x e. X |-> { x } ) )
35 vsnid 
 |-  z e. { z }
36 35 a1i 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. { z } )
37 24 snssd 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } C_ y )
38 eleq2 
 |-  ( w = { z } -> ( z e. w <-> z e. { z } ) )
39 sseq1 
 |-  ( w = { z } -> ( w C_ y <-> { z } C_ y ) )
40 38 39 anbi12d 
 |-  ( w = { z } -> ( ( z e. w /\ w C_ y ) <-> ( z e. { z } /\ { z } C_ y ) ) )
41 40 rspcev 
 |-  ( ( { z } e. ran ( x e. X |-> { x } ) /\ ( z e. { z } /\ { z } C_ y ) ) -> E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) )
42 34 36 37 41 syl12anc 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) )
43 42 ralrimivva 
 |-  ( X e. _V -> A. y e. ~P X A. z e. y E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) )
44 basgen2 
 |-  ( ( ~P X e. Top /\ ran ( x e. X |-> { x } ) C_ ~P X /\ A. y e. ~P X A. z e. y E. w e. ran ( x e. X |-> { x } ) ( z e. w /\ w C_ y ) ) -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
45 17 21 43 44 syl3anc 
 |-  ( X e. _V -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
46 45 adantr 
 |-  ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
47 45 17 eqeltrd 
 |-  ( X e. _V -> ( topGen ` ran ( x e. X |-> { x } ) ) e. Top )
48 tgclb 
 |-  ( ran ( x e. X |-> { x } ) e. TopBases <-> ( topGen ` ran ( x e. X |-> { x } ) ) e. Top )
49 47 48 sylibr 
 |-  ( X e. _V -> ran ( x e. X |-> { x } ) e. TopBases )
50 2ndci 
 |-  ( ( ran ( x e. X |-> { x } ) e. TopBases /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) e. 2ndc )
51 49 50 sylan 
 |-  ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) e. 2ndc )
52 46 51 eqeltrrd 
 |-  ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ~P X e. 2ndc )
53 is2ndc 
 |-  ( ~P X e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) )
54 vex 
 |-  b e. _V
55 18 bilani 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. ~P X )
56 simplrr 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> ( topGen ` b ) = ~P X )
57 55 56 eleqtrrd 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. ( topGen ` b ) )
58 vsnid 
 |-  x e. { x }
59 tg2 
 |-  ( ( { x } e. ( topGen ` b ) /\ x e. { x } ) -> E. y e. b ( x e. y /\ y C_ { x } ) )
60 57 58 59 sylancl 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> E. y e. b ( x e. y /\ y C_ { x } ) )
61 simprrl 
 |-  ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> x e. y )
62 61 snssd 
 |-  ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> { x } C_ y )
63 simprrr 
 |-  ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> y C_ { x } )
64 62 63 eqssd 
 |-  ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> { x } = y )
65 simprl 
 |-  ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> y e. b )
66 64 65 eqeltrd 
 |-  ( ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) /\ ( y e. b /\ ( x e. y /\ y C_ { x } ) ) ) -> { x } e. b )
67 60 66 rexlimddv 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. b )
68 67 fmpttd 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ( x e. X |-> { x } ) : X --> b )
69 68 frnd 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) C_ b )
70 ssdomg 
 |-  ( b e. _V -> ( ran ( x e. X |-> { x } ) C_ b -> ran ( x e. X |-> { x } ) ~<_ b ) )
71 54 69 70 mpsyl 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) ~<_ b )
72 simprl 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> b ~<_ _om )
73 domtr 
 |-  ( ( ran ( x e. X |-> { x } ) ~<_ b /\ b ~<_ _om ) -> ran ( x e. X |-> { x } ) ~<_ _om )
74 71 72 73 syl2anc 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) ~<_ _om )
75 74 rexlimdva2 
 |-  ( X e. _V -> ( E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) -> ran ( x e. X |-> { x } ) ~<_ _om ) )
76 53 75 biimtrid 
 |-  ( X e. _V -> ( ~P X e. 2ndc -> ran ( x e. X |-> { x } ) ~<_ _om ) )
77 76 imp 
 |-  ( ( X e. _V /\ ~P X e. 2ndc ) -> ran ( x e. X |-> { x } ) ~<_ _om )
78 52 77 impbida 
 |-  ( X e. _V -> ( ran ( x e. X |-> { x } ) ~<_ _om <-> ~P X e. 2ndc ) )
79 16 78 bitrd 
 |-  ( X e. _V -> ( X ~<_ _om <-> ~P X e. 2ndc ) )
80 1 2 79 pm5.21nii 
 |-  ( X ~<_ _om <-> ~P X e. 2ndc )