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 simpr 
 |-  ( ( X e. _V /\ x e. X ) -> x e. X )
19 5 snelpw 
 |-  ( x e. X <-> { x } e. ~P X )
20 18 19 sylib 
 |-  ( ( X e. _V /\ x e. X ) -> { x } e. ~P X )
21 20 fmpttd 
 |-  ( X e. _V -> ( x e. X |-> { x } ) : X --> ~P X )
22 21 frnd 
 |-  ( X e. _V -> ran ( x e. X |-> { x } ) C_ ~P X )
23 elpwi 
 |-  ( y e. ~P X -> y C_ X )
24 23 ad2antrl 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> y C_ X )
25 simprr 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. y )
26 24 25 sseldd 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. X )
27 eqidd 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } = { z } )
28 sneq 
 |-  ( x = z -> { x } = { z } )
29 28 rspceeqv 
 |-  ( ( z e. X /\ { z } = { z } ) -> E. x e. X { z } = { x } )
30 26 27 29 syl2anc 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> E. x e. X { z } = { x } )
31 vsnex 
 |-  { z } e. _V
32 eqid 
 |-  ( x e. X |-> { x } ) = ( x e. X |-> { x } )
33 32 elrnmpt 
 |-  ( { z } e. _V -> ( { z } e. ran ( x e. X |-> { x } ) <-> E. x e. X { z } = { x } ) )
34 31 33 ax-mp 
 |-  ( { z } e. ran ( x e. X |-> { x } ) <-> E. x e. X { z } = { x } )
35 30 34 sylibr 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } e. ran ( x e. X |-> { x } ) )
36 vsnid 
 |-  z e. { z }
37 36 a1i 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> z e. { z } )
38 25 snssd 
 |-  ( ( X e. _V /\ ( y e. ~P X /\ z e. y ) ) -> { z } C_ y )
39 eleq2 
 |-  ( w = { z } -> ( z e. w <-> z e. { z } ) )
40 sseq1 
 |-  ( w = { z } -> ( w C_ y <-> { z } C_ y ) )
41 39 40 anbi12d 
 |-  ( w = { z } -> ( ( z e. w /\ w C_ y ) <-> ( z e. { z } /\ { z } C_ y ) ) )
42 41 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 ) )
43 35 37 38 42 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 ) )
44 43 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 ) )
45 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 )
46 17 22 44 45 syl3anc 
 |-  ( X e. _V -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
47 46 adantr 
 |-  ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) = ~P X )
48 46 17 eqeltrd 
 |-  ( X e. _V -> ( topGen ` ran ( x e. X |-> { x } ) ) e. Top )
49 tgclb 
 |-  ( ran ( x e. X |-> { x } ) e. TopBases <-> ( topGen ` ran ( x e. X |-> { x } ) ) e. Top )
50 48 49 sylibr 
 |-  ( X e. _V -> ran ( x e. X |-> { x } ) e. TopBases )
51 2ndci 
 |-  ( ( ran ( x e. X |-> { x } ) e. TopBases /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) e. 2ndc )
52 50 51 sylan 
 |-  ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ( topGen ` ran ( x e. X |-> { x } ) ) e. 2ndc )
53 47 52 eqeltrrd 
 |-  ( ( X e. _V /\ ran ( x e. X |-> { x } ) ~<_ _om ) -> ~P X e. 2ndc )
54 is2ndc 
 |-  ( ~P X e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) )
55 vex 
 |-  b e. _V
56 simpr 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> x e. X )
57 56 19 sylib 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. ~P X )
58 simplrr 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> ( topGen ` b ) = ~P X )
59 57 58 eleqtrrd 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. ( topGen ` b ) )
60 vsnid 
 |-  x e. { x }
61 tg2 
 |-  ( ( { x } e. ( topGen ` b ) /\ x e. { x } ) -> E. y e. b ( x e. y /\ y C_ { x } ) )
62 59 60 61 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 } ) )
63 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 )
64 63 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 )
65 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 } )
66 64 65 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 )
67 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 )
68 66 67 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 )
69 62 68 rexlimddv 
 |-  ( ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) /\ x e. X ) -> { x } e. b )
70 69 fmpttd 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ( x e. X |-> { x } ) : X --> b )
71 70 frnd 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) C_ b )
72 ssdomg 
 |-  ( b e. _V -> ( ran ( x e. X |-> { x } ) C_ b -> ran ( x e. X |-> { x } ) ~<_ b ) )
73 55 71 72 mpsyl 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) ~<_ b )
74 simprl 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> b ~<_ _om )
75 domtr 
 |-  ( ( ran ( x e. X |-> { x } ) ~<_ b /\ b ~<_ _om ) -> ran ( x e. X |-> { x } ) ~<_ _om )
76 73 74 75 syl2anc 
 |-  ( ( ( X e. _V /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) ) -> ran ( x e. X |-> { x } ) ~<_ _om )
77 76 rexlimdva2 
 |-  ( X e. _V -> ( E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = ~P X ) -> ran ( x e. X |-> { x } ) ~<_ _om ) )
78 54 77 biimtrid 
 |-  ( X e. _V -> ( ~P X e. 2ndc -> ran ( x e. X |-> { x } ) ~<_ _om ) )
79 78 imp 
 |-  ( ( X e. _V /\ ~P X e. 2ndc ) -> ran ( x e. X |-> { x } ) ~<_ _om )
80 53 79 impbida 
 |-  ( X e. _V -> ( ran ( x e. X |-> { x } ) ~<_ _om <-> ~P X e. 2ndc ) )
81 16 80 bitrd 
 |-  ( X e. _V -> ( X ~<_ _om <-> ~P X e. 2ndc ) )
82 1 2 81 pm5.21nii 
 |-  ( X ~<_ _om <-> ~P X e. 2ndc )