Metamath Proof Explorer

Theorem 2ndc1stc

Description: A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010)

Ref Expression
Assertion 2ndc1stc 
|- ( J e. 2ndc -> J e. 1stc )

Proof

Step Hyp Ref Expression
1 2ndctop 
 |-  ( J e. 2ndc -> J e. Top )
2 is2ndc 
 |-  ( J e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) )
3 ssrab2 
 |-  { q e. b | x e. q } C_ b
4 bastg 
 |-  ( b e. TopBases -> b C_ ( topGen ` b ) )
5 4 3ad2ant1 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> b C_ ( topGen ` b ) )
6 3 5 sstrid 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> { q e. b | x e. q } C_ ( topGen ` b ) )
7 fvex 
 |-  ( topGen ` b ) e. _V
8 7 elpw2 
 |-  ( { q e. b | x e. q } e. ~P ( topGen ` b ) <-> { q e. b | x e. q } C_ ( topGen ` b ) )
9 6 8 sylibr 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> { q e. b | x e. q } e. ~P ( topGen ` b ) )
10 vex 
 |-  b e. _V
11 ssdomg 
 |-  ( b e. _V -> ( { q e. b | x e. q } C_ b -> { q e. b | x e. q } ~<_ b ) )
12 10 3 11 mp2 
 |-  { q e. b | x e. q } ~<_ b
13 simp2 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> b ~<_ _om )
14 domtr 
 |-  ( ( { q e. b | x e. q } ~<_ b /\ b ~<_ _om ) -> { q e. b | x e. q } ~<_ _om )
15 12 13 14 sylancr 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> { q e. b | x e. q } ~<_ _om )
16 eltg2b 
 |-  ( b e. TopBases -> ( o e. ( topGen ` b ) <-> A. y e. o E. t e. b ( y e. t /\ t C_ o ) ) )
17 16 3ad2ant1 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> ( o e. ( topGen ` b ) <-> A. y e. o E. t e. b ( y e. t /\ t C_ o ) ) )
18 elequ1 
 |-  ( y = x -> ( y e. t <-> x e. t ) )
19 18 anbi1d 
 |-  ( y = x -> ( ( y e. t /\ t C_ o ) <-> ( x e. t /\ t C_ o ) ) )
20 19 rexbidv 
 |-  ( y = x -> ( E. t e. b ( y e. t /\ t C_ o ) <-> E. t e. b ( x e. t /\ t C_ o ) ) )
21 20 rspccv 
 |-  ( A. y e. o E. t e. b ( y e. t /\ t C_ o ) -> ( x e. o -> E. t e. b ( x e. t /\ t C_ o ) ) )
22 id 
 |-  ( ( t e. b /\ x e. t ) -> ( t e. b /\ x e. t ) )
23 22 adantrr 
 |-  ( ( t e. b /\ ( x e. t /\ t C_ o ) ) -> ( t e. b /\ x e. t ) )
24 elequ2 
 |-  ( q = t -> ( x e. q <-> x e. t ) )
25 24 elrab 
 |-  ( t e. { q e. b | x e. q } <-> ( t e. b /\ x e. t ) )
26 23 25 sylibr 
 |-  ( ( t e. b /\ ( x e. t /\ t C_ o ) ) -> t e. { q e. b | x e. q } )
27 simprr 
 |-  ( ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) /\ ( t e. b /\ ( x e. t /\ t C_ o ) ) ) -> ( x e. t /\ t C_ o ) )
28 elequ2 
 |-  ( p = t -> ( x e. p <-> x e. t ) )
29 sseq1 
 |-  ( p = t -> ( p C_ o <-> t C_ o ) )
30 28 29 anbi12d 
 |-  ( p = t -> ( ( x e. p /\ p C_ o ) <-> ( x e. t /\ t C_ o ) ) )
31 30 rspcev 
 |-  ( ( t e. { q e. b | x e. q } /\ ( x e. t /\ t C_ o ) ) -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) )
32 26 27 31 syl2an2 
 |-  ( ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) /\ ( t e. b /\ ( x e. t /\ t C_ o ) ) ) -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) )
33 32 rexlimdvaa 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> ( E. t e. b ( x e. t /\ t C_ o ) -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) )
34 21 33 syl9r 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> ( A. y e. o E. t e. b ( y e. t /\ t C_ o ) -> ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) ) )
35 17 34 sylbid 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> ( o e. ( topGen ` b ) -> ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) ) )
36 35 ralrimiv 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> A. o e. ( topGen ` b ) ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) )
37 breq1 
 |-  ( s = { q e. b | x e. q } -> ( s ~<_ _om <-> { q e. b | x e. q } ~<_ _om ) )
38 rexeq 
 |-  ( s = { q e. b | x e. q } -> ( E. p e. s ( x e. p /\ p C_ o ) <-> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) )
39 38 imbi2d 
 |-  ( s = { q e. b | x e. q } -> ( ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) <-> ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) ) )
40 39 ralbidv 
 |-  ( s = { q e. b | x e. q } -> ( A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) <-> A. o e. ( topGen ` b ) ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) ) )
41 37 40 anbi12d 
 |-  ( s = { q e. b | x e. q } -> ( ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) <-> ( { q e. b | x e. q } ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) ) ) )
42 41 rspcev 
 |-  ( ( { q e. b | x e. q } e. ~P ( topGen ` b ) /\ ( { q e. b | x e. q } ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. { q e. b | x e. q } ( x e. p /\ p C_ o ) ) ) ) -> E. s e. ~P ( topGen ` b ) ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) )
43 9 15 36 42 syl12anc 
 |-  ( ( b e. TopBases /\ b ~<_ _om /\ x e. U. ( topGen ` b ) ) -> E. s e. ~P ( topGen ` b ) ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) )
44 43 3expia 
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> ( x e. U. ( topGen ` b ) -> E. s e. ~P ( topGen ` b ) ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) )
45 unieq 
 |-  ( ( topGen ` b ) = J -> U. ( topGen ` b ) = U. J )
46 45 eleq2d 
 |-  ( ( topGen ` b ) = J -> ( x e. U. ( topGen ` b ) <-> x e. U. J ) )
47 pweq 
 |-  ( ( topGen ` b ) = J -> ~P ( topGen ` b ) = ~P J )
48 raleq 
 |-  ( ( topGen ` b ) = J -> ( A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) <-> A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) )
49 48 anbi2d 
 |-  ( ( topGen ` b ) = J -> ( ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) <-> ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) )
50 47 49 rexeqbidv 
 |-  ( ( topGen ` b ) = J -> ( E. s e. ~P ( topGen ` b ) ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) <-> E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) )
51 46 50 imbi12d 
 |-  ( ( topGen ` b ) = J -> ( ( x e. U. ( topGen ` b ) -> E. s e. ~P ( topGen ` b ) ( s ~<_ _om /\ A. o e. ( topGen ` b ) ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) <-> ( x e. U. J -> E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) ) )
52 44 51 syl5ibcom 
 |-  ( ( b e. TopBases /\ b ~<_ _om ) -> ( ( topGen ` b ) = J -> ( x e. U. J -> E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) ) )
53 52 expimpd 
 |-  ( b e. TopBases -> ( ( b ~<_ _om /\ ( topGen ` b ) = J ) -> ( x e. U. J -> E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) ) )
54 53 rexlimiv 
 |-  ( E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) -> ( x e. U. J -> E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) )
55 2 54 sylbi 
 |-  ( J e. 2ndc -> ( x e. U. J -> E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) )
56 55 ralrimiv 
 |-  ( J e. 2ndc -> A. x e. U. J E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) )
57 eqid 
 |-  U. J = U. J
58 57 is1stc2 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. x e. U. J E. s e. ~P J ( s ~<_ _om /\ A. o e. J ( x e. o -> E. p e. s ( x e. p /\ p C_ o ) ) ) ) )
59 1 56 58 sylanbrc 
 |-  ( J e. 2ndc -> J e. 1stc )