Metamath Proof Explorer

Theorem met1stc

Description: The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis methaus.1 
|- J = ( MetOpen ` D )
Assertion met1stc 
|- ( D e. ( *Met ` X ) -> J e. 1stc )

Proof

Step Hyp Ref Expression
1 methaus.1 
 |-  J = ( MetOpen ` D )
2 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
3 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
4 3 eleq2d 
 |-  ( D e. ( *Met ` X ) -> ( x e. X <-> x e. U. J ) )
5 4 biimpar 
 |-  ( ( D e. ( *Met ` X ) /\ x e. U. J ) -> x e. X )
6 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ n e. NN ) -> D e. ( *Met ` X ) )
7 simplr 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ n e. NN ) -> x e. X )
8 nnrp 
 |-  ( n e. NN -> n e. RR+ )
9 8 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ n e. NN ) -> n e. RR+ )
10 9 rpreccld 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ n e. NN ) -> ( 1 / n ) e. RR+ )
11 10 rpxrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ n e. NN ) -> ( 1 / n ) e. RR* )
12 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( 1 / n ) e. RR* ) -> ( x ( ball ` D ) ( 1 / n ) ) e. J )
13 6 7 11 12 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ n e. NN ) -> ( x ( ball ` D ) ( 1 / n ) ) e. J )
14 13 fmpttd 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) : NN --> J )
15 14 frnd 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) C_ J )
16 nnex 
 |-  NN e. _V
17 16 mptex 
 |-  ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) e. _V
18 17 rnex 
 |-  ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) e. _V
19 18 elpw 
 |-  ( ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) e. ~P J <-> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) C_ J )
20 15 19 sylibr 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) e. ~P J )
21 omelon 
 |-  _om e. On
22 nnenom 
 |-  NN ~~ _om
23 22 ensymi 
 |-  _om ~~ NN
24 isnumi 
 |-  ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card )
25 21 23 24 mp2an 
 |-  NN e. dom card
26 ovex 
 |-  ( x ( ball ` D ) ( 1 / n ) ) e. _V
27 eqid 
 |-  ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) = ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) )
28 26 27 fnmpti 
 |-  ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) Fn NN
29 dffn4 
 |-  ( ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) Fn NN <-> ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) : NN -onto-> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) )
30 28 29 mpbi 
 |-  ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) : NN -onto-> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) )
31 fodomnum 
 |-  ( NN e. dom card -> ( ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) : NN -onto-> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) -> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ NN ) )
32 25 30 31 mp2 
 |-  ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ NN
33 domentr 
 |-  ( ( ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ NN /\ NN ~~ _om ) -> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ _om )
34 32 22 33 mp2an 
 |-  ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ _om
35 34 a1i 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ _om )
36 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> D e. ( *Met ` X ) )
37 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> z e. J )
38 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> x e. z )
39 1 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ z e. J /\ x e. z ) -> E. r e. RR+ ( x ( ball ` D ) r ) C_ z )
40 36 37 38 39 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> E. r e. RR+ ( x ( ball ` D ) r ) C_ z )
41 simp-4l 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> D e. ( *Met ` X ) )
42 simp-4r 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> x e. X )
43 simprl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> y e. NN )
44 43 nnrpd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> y e. RR+ )
45 44 rpreccld 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( 1 / y ) e. RR+ )
46 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( 1 / y ) e. RR+ ) -> x e. ( x ( ball ` D ) ( 1 / y ) ) )
47 41 42 45 46 syl3anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> x e. ( x ( ball ` D ) ( 1 / y ) ) )
48 45 rpxrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( 1 / y ) e. RR* )
49 simplrl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> r e. RR+ )
50 49 rpxrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> r e. RR* )
51 nnrecre 
 |-  ( y e. NN -> ( 1 / y ) e. RR )
52 51 ad2antrl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( 1 / y ) e. RR )
53 49 rpred 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> r e. RR )
54 simprr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( 1 / y ) < r )
55 52 53 54 ltled 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( 1 / y ) <_ r )
56 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( ( 1 / y ) e. RR* /\ r e. RR* ) /\ ( 1 / y ) <_ r ) -> ( x ( ball ` D ) ( 1 / y ) ) C_ ( x ( ball ` D ) r ) )
57 41 42 48 50 55 56 syl221anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( x ( ball ` D ) ( 1 / y ) ) C_ ( x ( ball ` D ) r ) )
58 simplrr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( x ( ball ` D ) r ) C_ z )
59 57 58 sstrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( x ( ball ` D ) ( 1 / y ) ) C_ z )
60 47 59 jca 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) /\ ( y e. NN /\ ( 1 / y ) < r ) ) -> ( x e. ( x ( ball ` D ) ( 1 / y ) ) /\ ( x ( ball ` D ) ( 1 / y ) ) C_ z ) )
61 elrp 
 |-  ( r e. RR+ <-> ( r e. RR /\ 0 < r ) )
62 nnrecl 
 |-  ( ( r e. RR /\ 0 < r ) -> E. y e. NN ( 1 / y ) < r )
63 61 62 sylbi 
 |-  ( r e. RR+ -> E. y e. NN ( 1 / y ) < r )
64 63 ad2antrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) -> E. y e. NN ( 1 / y ) < r )
65 60 64 reximddv 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ z ) ) -> E. y e. NN ( x e. ( x ( ball ` D ) ( 1 / y ) ) /\ ( x ( ball ` D ) ( 1 / y ) ) C_ z ) )
66 40 65 rexlimddv 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> E. y e. NN ( x e. ( x ( ball ` D ) ( 1 / y ) ) /\ ( x ( ball ` D ) ( 1 / y ) ) C_ z ) )
67 ovexd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ y e. NN ) -> ( x ( ball ` D ) ( 1 / y ) ) e. _V )
68 vex 
 |-  w e. _V
69 oveq2 
 |-  ( n = y -> ( 1 / n ) = ( 1 / y ) )
70 69 oveq2d 
 |-  ( n = y -> ( x ( ball ` D ) ( 1 / n ) ) = ( x ( ball ` D ) ( 1 / y ) ) )
71 70 cbvmptv 
 |-  ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) = ( y e. NN |-> ( x ( ball ` D ) ( 1 / y ) ) )
72 71 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) <-> E. y e. NN w = ( x ( ball ` D ) ( 1 / y ) ) ) )
73 68 72 mp1i 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> ( w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) <-> E. y e. NN w = ( x ( ball ` D ) ( 1 / y ) ) ) )
74 eleq2 
 |-  ( w = ( x ( ball ` D ) ( 1 / y ) ) -> ( x e. w <-> x e. ( x ( ball ` D ) ( 1 / y ) ) ) )
75 sseq1 
 |-  ( w = ( x ( ball ` D ) ( 1 / y ) ) -> ( w C_ z <-> ( x ( ball ` D ) ( 1 / y ) ) C_ z ) )
76 74 75 anbi12d 
 |-  ( w = ( x ( ball ` D ) ( 1 / y ) ) -> ( ( x e. w /\ w C_ z ) <-> ( x e. ( x ( ball ` D ) ( 1 / y ) ) /\ ( x ( ball ` D ) ( 1 / y ) ) C_ z ) ) )
77 76 adantl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) /\ w = ( x ( ball ` D ) ( 1 / y ) ) ) -> ( ( x e. w /\ w C_ z ) <-> ( x e. ( x ( ball ` D ) ( 1 / y ) ) /\ ( x ( ball ` D ) ( 1 / y ) ) C_ z ) ) )
78 67 73 77 rexxfr2d 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> ( E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) <-> E. y e. NN ( x e. ( x ( ball ` D ) ( 1 / y ) ) /\ ( x ( ball ` D ) ( 1 / y ) ) C_ z ) ) )
79 66 78 mpbird 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( z e. J /\ x e. z ) ) -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) )
80 79 expr 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ z e. J ) -> ( x e. z -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) )
81 80 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> A. z e. J ( x e. z -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) )
82 breq1 
 |-  ( y = ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) -> ( y ~<_ _om <-> ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ _om ) )
83 rexeq 
 |-  ( y = ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) -> ( E. w e. y ( x e. w /\ w C_ z ) <-> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) )
84 83 imbi2d 
 |-  ( y = ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) -> ( ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> ( x e. z -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) ) )
85 84 ralbidv 
 |-  ( y = ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) -> ( A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> A. z e. J ( x e. z -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) ) )
86 82 85 anbi12d 
 |-  ( y = ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) -> ( ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> ( ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ _om /\ A. z e. J ( x e. z -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) ) ) )
87 86 rspcev 
 |-  ( ( ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) e. ~P J /\ ( ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ~<_ _om /\ A. z e. J ( x e. z -> E. w e. ran ( n e. NN |-> ( x ( ball ` D ) ( 1 / n ) ) ) ( x e. w /\ w C_ z ) ) ) ) -> E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
88 20 35 81 87 syl12anc 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
89 5 88 syldan 
 |-  ( ( D e. ( *Met ` X ) /\ x e. U. J ) -> E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
90 89 ralrimiva 
 |-  ( D e. ( *Met ` X ) -> A. x e. U. J E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
91 eqid 
 |-  U. J = U. J
92 91 is1stc2 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. x e. U. J E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )
93 2 90 92 sylanbrc 
 |-  ( D e. ( *Met ` X ) -> J e. 1stc )