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 ) )