Metamath Proof Explorer


Theorem 2ndcsep

Description: A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis 2ndcsep.1
|- X = U. J
Assertion 2ndcsep
|- ( J e. 2ndc -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) )

Proof

Step Hyp Ref Expression
1 2ndcsep.1
 |-  X = U. J
2 is2ndc
 |-  ( J e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) )
3 vex
 |-  b e. _V
4 difss
 |-  ( b \ { (/) } ) C_ b
5 ssdomg
 |-  ( b e. _V -> ( ( b \ { (/) } ) C_ b -> ( b \ { (/) } ) ~<_ b ) )
6 3 4 5 mp2
 |-  ( b \ { (/) } ) ~<_ b
7 simpr
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> b ~<_ _om )
8 domtr
 |-  ( ( ( b \ { (/) } ) ~<_ b /\ b ~<_ _om ) -> ( b \ { (/) } ) ~<_ _om )
9 6 7 8 sylancr
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> ( b \ { (/) } ) ~<_ _om )
10 eldifsn
 |-  ( y e. ( b \ { (/) } ) <-> ( y e. b /\ y =/= (/) ) )
11 n0
 |-  ( y =/= (/) <-> E. z z e. y )
12 elunii
 |-  ( ( z e. y /\ y e. b ) -> z e. U. b )
13 simpl
 |-  ( ( z e. y /\ y e. b ) -> z e. y )
14 12 13 jca
 |-  ( ( z e. y /\ y e. b ) -> ( z e. U. b /\ z e. y ) )
15 14 expcom
 |-  ( y e. b -> ( z e. y -> ( z e. U. b /\ z e. y ) ) )
16 15 eximdv
 |-  ( y e. b -> ( E. z z e. y -> E. z ( z e. U. b /\ z e. y ) ) )
17 16 imp
 |-  ( ( y e. b /\ E. z z e. y ) -> E. z ( z e. U. b /\ z e. y ) )
18 df-rex
 |-  ( E. z e. U. b z e. y <-> E. z ( z e. U. b /\ z e. y ) )
19 17 18 sylibr
 |-  ( ( y e. b /\ E. z z e. y ) -> E. z e. U. b z e. y )
20 11 19 sylan2b
 |-  ( ( y e. b /\ y =/= (/) ) -> E. z e. U. b z e. y )
21 10 20 sylbi
 |-  ( y e. ( b \ { (/) } ) -> E. z e. U. b z e. y )
22 21 rgen
 |-  A. y e. ( b \ { (/) } ) E. z e. U. b z e. y
23 vuniex
 |-  U. b e. _V
24 eleq1
 |-  ( z = ( f ` y ) -> ( z e. y <-> ( f ` y ) e. y ) )
25 23 24 axcc4dom
 |-  ( ( ( b \ { (/) } ) ~<_ _om /\ A. y e. ( b \ { (/) } ) E. z e. U. b z e. y ) -> E. f ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) )
26 9 22 25 sylancl
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> E. f ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) )
27 frn
 |-  ( f : ( b \ { (/) } ) --> U. b -> ran f C_ U. b )
28 27 ad2antrl
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f C_ U. b )
29 vex
 |-  f e. _V
30 29 rnex
 |-  ran f e. _V
31 30 elpw
 |-  ( ran f e. ~P U. b <-> ran f C_ U. b )
32 28 31 sylibr
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f e. ~P U. b )
33 omelon
 |-  _om e. On
34 7 adantr
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> b ~<_ _om )
35 ondomen
 |-  ( ( _om e. On /\ b ~<_ _om ) -> b e. dom card )
36 33 34 35 sylancr
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> b e. dom card )
37 ssnum
 |-  ( ( b e. dom card /\ ( b \ { (/) } ) C_ b ) -> ( b \ { (/) } ) e. dom card )
38 36 4 37 sylancl
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( b \ { (/) } ) e. dom card )
39 ffn
 |-  ( f : ( b \ { (/) } ) --> U. b -> f Fn ( b \ { (/) } ) )
40 39 ad2antrl
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> f Fn ( b \ { (/) } ) )
41 dffn4
 |-  ( f Fn ( b \ { (/) } ) <-> f : ( b \ { (/) } ) -onto-> ran f )
42 40 41 sylib
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> f : ( b \ { (/) } ) -onto-> ran f )
43 fodomnum
 |-  ( ( b \ { (/) } ) e. dom card -> ( f : ( b \ { (/) } ) -onto-> ran f -> ran f ~<_ ( b \ { (/) } ) ) )
44 38 42 43 sylc
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f ~<_ ( b \ { (/) } ) )
45 9 adantr
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( b \ { (/) } ) ~<_ _om )
46 domtr
 |-  ( ( ran f ~<_ ( b \ { (/) } ) /\ ( b \ { (/) } ) ~<_ _om ) -> ran f ~<_ _om )
47 44 45 46 syl2anc
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f ~<_ _om )
48 tgcl
 |-  ( b e. TopBases -> ( topGen ` b ) e. Top )
49 48 ad2antrr
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( topGen ` b ) e. Top )
50 unitg
 |-  ( b e. _V -> U. ( topGen ` b ) = U. b )
51 50 elv
 |-  U. ( topGen ` b ) = U. b
52 51 eqcomi
 |-  U. b = U. ( topGen ` b )
53 52 clsss3
 |-  ( ( ( topGen ` b ) e. Top /\ ran f C_ U. b ) -> ( ( cls ` ( topGen ` b ) ) ` ran f ) C_ U. b )
54 49 28 53 syl2anc
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( ( cls ` ( topGen ` b ) ) ` ran f ) C_ U. b )
55 ne0i
 |-  ( x e. y -> y =/= (/) )
56 55 anim2i
 |-  ( ( y e. b /\ x e. y ) -> ( y e. b /\ y =/= (/) ) )
57 56 10 sylibr
 |-  ( ( y e. b /\ x e. y ) -> y e. ( b \ { (/) } ) )
58 fnfvelrn
 |-  ( ( f Fn ( b \ { (/) } ) /\ y e. ( b \ { (/) } ) ) -> ( f ` y ) e. ran f )
59 39 58 sylan
 |-  ( ( f : ( b \ { (/) } ) --> U. b /\ y e. ( b \ { (/) } ) ) -> ( f ` y ) e. ran f )
60 inelcm
 |-  ( ( ( f ` y ) e. y /\ ( f ` y ) e. ran f ) -> ( y i^i ran f ) =/= (/) )
61 60 expcom
 |-  ( ( f ` y ) e. ran f -> ( ( f ` y ) e. y -> ( y i^i ran f ) =/= (/) ) )
62 59 61 syl
 |-  ( ( f : ( b \ { (/) } ) --> U. b /\ y e. ( b \ { (/) } ) ) -> ( ( f ` y ) e. y -> ( y i^i ran f ) =/= (/) ) )
63 62 ex
 |-  ( f : ( b \ { (/) } ) --> U. b -> ( y e. ( b \ { (/) } ) -> ( ( f ` y ) e. y -> ( y i^i ran f ) =/= (/) ) ) )
64 63 a2d
 |-  ( f : ( b \ { (/) } ) --> U. b -> ( ( y e. ( b \ { (/) } ) -> ( f ` y ) e. y ) -> ( y e. ( b \ { (/) } ) -> ( y i^i ran f ) =/= (/) ) ) )
65 57 64 syl7
 |-  ( f : ( b \ { (/) } ) --> U. b -> ( ( y e. ( b \ { (/) } ) -> ( f ` y ) e. y ) -> ( ( y e. b /\ x e. y ) -> ( y i^i ran f ) =/= (/) ) ) )
66 65 exp4a
 |-  ( f : ( b \ { (/) } ) --> U. b -> ( ( y e. ( b \ { (/) } ) -> ( f ` y ) e. y ) -> ( y e. b -> ( x e. y -> ( y i^i ran f ) =/= (/) ) ) ) )
67 66 ralimdv2
 |-  ( f : ( b \ { (/) } ) --> U. b -> ( A. y e. ( b \ { (/) } ) ( f ` y ) e. y -> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) ) )
68 67 imp
 |-  ( ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) -> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) )
69 68 ad2antlr
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) )
70 eqidd
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> ( topGen ` b ) = ( topGen ` b ) )
71 52 a1i
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> U. b = U. ( topGen ` b ) )
72 simplll
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> b e. TopBases )
73 28 adantr
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> ran f C_ U. b )
74 simpr
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> x e. U. b )
75 70 71 72 73 74 elcls3
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> ( x e. ( ( cls ` ( topGen ` b ) ) ` ran f ) <-> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) ) )
76 69 75 mpbird
 |-  ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> x e. ( ( cls ` ( topGen ` b ) ) ` ran f ) )
77 54 76 eqelssd
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b )
78 breq1
 |-  ( x = ran f -> ( x ~<_ _om <-> ran f ~<_ _om ) )
79 fveqeq2
 |-  ( x = ran f -> ( ( ( cls ` ( topGen ` b ) ) ` x ) = U. b <-> ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) )
80 78 79 anbi12d
 |-  ( x = ran f -> ( ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) <-> ( ran f ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) ) )
81 80 rspcev
 |-  ( ( ran f e. ~P U. b /\ ( ran f ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) ) -> E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) )
82 32 47 77 81 syl12anc
 |-  ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) )
83 26 82 exlimddv
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) )
84 unieq
 |-  ( ( topGen ` b ) = J -> U. ( topGen ` b ) = U. J )
85 84 52 1 3eqtr4g
 |-  ( ( topGen ` b ) = J -> U. b = X )
86 85 pweqd
 |-  ( ( topGen ` b ) = J -> ~P U. b = ~P X )
87 fveq2
 |-  ( ( topGen ` b ) = J -> ( cls ` ( topGen ` b ) ) = ( cls ` J ) )
88 87 fveq1d
 |-  ( ( topGen ` b ) = J -> ( ( cls ` ( topGen ` b ) ) ` x ) = ( ( cls ` J ) ` x ) )
89 88 85 eqeq12d
 |-  ( ( topGen ` b ) = J -> ( ( ( cls ` ( topGen ` b ) ) ` x ) = U. b <-> ( ( cls ` J ) ` x ) = X ) )
90 89 anbi2d
 |-  ( ( topGen ` b ) = J -> ( ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) <-> ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) )
91 86 90 rexeqbidv
 |-  ( ( topGen ` b ) = J -> ( E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) <-> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) )
92 83 91 syl5ibcom
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> ( ( topGen ` b ) = J -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) )
93 92 impr
 |-  ( ( b e. TopBases /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) )
94 93 rexlimiva
 |-  ( E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) )
95 2 94 sylbi
 |-  ( J e. 2ndc -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) )