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 )