MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  met2ndci Unicode version

Theorem met2ndci 18164
Description: A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
Hypothesis
Ref Expression
methaus.1  |-  J  =  ( MetOpen `  D )
Assertion
Ref Expression
met2ndci  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  J  e.  2ndc )

Proof of Theorem met2ndci
Dummy variables  n  r  t  u  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 methaus.1 . . . . 5  |-  J  =  ( MetOpen `  D )
21mopntop 18082 . . . 4  |-  ( D  e.  ( * Met `  X )  ->  J  e.  Top )
32adantr 451 . . 3  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  J  e.  Top )
4 simpll 730 . . . . . . 7  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  ->  D  e.  ( * Met `  X ) )
5 simplr1 997 . . . . . . . 8  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  ->  A  C_  X )
6 simprr 733 . . . . . . . 8  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  -> 
y  e.  A )
75, 6sseldd 3257 . . . . . . 7  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  -> 
y  e.  X )
8 simprl 732 . . . . . . . . . 10  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  ->  x  e.  NN )
98nnrpd 10478 . . . . . . . . 9  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  ->  x  e.  RR+ )
109rpreccld 10489 . . . . . . . 8  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  -> 
( 1  /  x
)  e.  RR+ )
1110rpxrd 10480 . . . . . . 7  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  -> 
( 1  /  x
)  e.  RR* )
121blopn 18142 . . . . . . 7  |-  ( ( D  e.  ( * Met `  X )  /\  y  e.  X  /\  ( 1  /  x
)  e.  RR* )  ->  ( y ( ball `  D ) ( 1  /  x ) )  e.  J )
134, 7, 11, 12syl3anc 1182 . . . . . 6  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( x  e.  NN  /\  y  e.  A ) )  -> 
( y ( ball `  D ) ( 1  /  x ) )  e.  J )
1413ralrimivva 2711 . . . . 5  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  A. x  e.  NN  A. y  e.  A  ( y ( ball `  D
) ( 1  /  x ) )  e.  J )
15 eqid 2358 . . . . . 6  |-  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) )  =  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) )
1615fmpt2 6275 . . . . 5  |-  ( A. x  e.  NN  A. y  e.  A  ( y
( ball `  D )
( 1  /  x
) )  e.  J  <->  ( x  e.  NN , 
y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) : ( NN  X.  A ) --> J )
1714, 16sylib 188 . . . 4  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) : ( NN 
X.  A ) --> J )
18 frn 5475 . . . 4  |-  ( ( x  e.  NN , 
y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) : ( NN  X.  A ) --> J  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  C_  J )
1917, 18syl 15 . . 3  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  C_  J )
20 simpll 730 . . . . . 6  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  ->  D  e.  ( * Met `  X ) )
21 simprl 732 . . . . . 6  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  ->  u  e.  J )
22 simprr 733 . . . . . 6  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  -> 
z  e.  u )
231mopni2 18135 . . . . . 6  |-  ( ( D  e.  ( * Met `  X )  /\  u  e.  J  /\  z  e.  u
)  ->  E. r  e.  RR+  ( z (
ball `  D )
r )  C_  u
)
2420, 21, 22, 23syl3anc 1182 . . . . 5  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  ->  E. r  e.  RR+  (
z ( ball `  D
) r )  C_  u )
25 simprl 732 . . . . . . . . . 10  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  ->  r  e.  RR+ )
2625rphalfcld 10491 . . . . . . . . 9  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  ->  ( r  / 
2 )  e.  RR+ )
27 elrp 10445 . . . . . . . . . 10  |-  ( ( r  /  2 )  e.  RR+  <->  ( ( r  /  2 )  e.  RR  /\  0  < 
( r  /  2
) ) )
28 nnrecl 10052 . . . . . . . . . 10  |-  ( ( ( r  /  2
)  e.  RR  /\  0  <  ( r  / 
2 ) )  ->  E. n  e.  NN  ( 1  /  n
)  <  ( r  /  2 ) )
2927, 28sylbi 187 . . . . . . . . 9  |-  ( ( r  /  2 )  e.  RR+  ->  E. n  e.  NN  ( 1  /  n )  <  (
r  /  2 ) )
3026, 29syl 15 . . . . . . . 8  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  ->  E. n  e.  NN  ( 1  /  n
)  <  ( r  /  2 ) )
313ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  J  e.  Top )
32 simpr1 961 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  A  C_  X )
3332ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  A  C_  X
)
341mopnuni 18083 . . . . . . . . . . . . . . . 16  |-  ( D  e.  ( * Met `  X )  ->  X  =  U. J )
3534ad3antrrr 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  X  =  U. J )
3633, 35sseqtrd 3290 . . . . . . . . . . . . . 14  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  A  C_  U. J
)
37 simplrr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  z  e.  u
)
38 simplrl 736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  u  e.  J
)
39 elunii 3911 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  u  /\  u  e.  J )  ->  z  e.  U. J
)
4037, 38, 39syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  z  e.  U. J )
4140, 35eleqtrrd 2435 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  z  e.  X
)
42 simpr3 963 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( ( cls `  J
) `  A )  =  X )
4342ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( ( cls `  J ) `  A
)  =  X )
4441, 43eleqtrrd 2435 . . . . . . . . . . . . . 14  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  z  e.  ( ( cls `  J
) `  A )
)
4520adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  D  e.  ( * Met `  X
) )
46 simprrl 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  n  e.  NN )
4746nnrpd 10478 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  n  e.  RR+ )
4847rpreccld 10489 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( 1  /  n )  e.  RR+ )
4948rpxrd 10480 . . . . . . . . . . . . . . 15  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( 1  /  n )  e.  RR* )
501blopn 18142 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( * Met `  X )  /\  z  e.  X  /\  ( 1  /  n
)  e.  RR* )  ->  ( z ( ball `  D ) ( 1  /  n ) )  e.  J )
5145, 41, 49, 50syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( z (
ball `  D )
( 1  /  n
) )  e.  J
)
52 blcntr 18060 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( * Met `  X )  /\  z  e.  X  /\  ( 1  /  n
)  e.  RR+ )  ->  z  e.  ( z ( ball `  D
) ( 1  /  n ) ) )
5345, 41, 48, 52syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  z  e.  ( z ( ball `  D
) ( 1  /  n ) ) )
54 eqid 2358 . . . . . . . . . . . . . . 15  |-  U. J  =  U. J
5554clsndisj 16912 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  Top  /\  A  C_  U. J  /\  z  e.  ( ( cls `  J ) `  A ) )  /\  ( ( z (
ball `  D )
( 1  /  n
) )  e.  J  /\  z  e.  (
z ( ball `  D
) ( 1  /  n ) ) ) )  ->  ( (
z ( ball `  D
) ( 1  /  n ) )  i^i 
A )  =/=  (/) )
5631, 36, 44, 51, 53, 55syl32anc 1190 . . . . . . . . . . . . 13  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( ( z ( ball `  D
) ( 1  /  n ) )  i^i 
A )  =/=  (/) )
57 n0 3540 . . . . . . . . . . . . 13  |-  ( ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A )  =/=  (/) 
<->  E. t  t  e.  ( ( z (
ball `  D )
( 1  /  n
) )  i^i  A
) )
5856, 57sylib 188 . . . . . . . . . . . 12  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  E. t  t  e.  ( ( z (
ball `  D )
( 1  /  n
) )  i^i  A
) )
5946adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  n  e.  NN )
60 inss2 3466 . . . . . . . . . . . . . . . . . 18  |-  ( ( z ( ball `  D
) ( 1  /  n ) )  i^i 
A )  C_  A
61 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )
6260, 61sseldi 3254 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  t  e.  A
)
63 eqidd 2359 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t (
ball `  D )
( 1  /  n
) )  =  ( t ( ball `  D
) ( 1  /  n ) ) )
64 oveq2 5950 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  n  ->  (
1  /  x )  =  ( 1  /  n ) )
6564oveq2d 5958 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  n  ->  (
y ( ball `  D
) ( 1  /  x ) )  =  ( y ( ball `  D ) ( 1  /  n ) ) )
6665eqeq2d 2369 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  n  ->  (
( t ( ball `  D ) ( 1  /  n ) )  =  ( y (
ball `  D )
( 1  /  x
) )  <->  ( t
( ball `  D )
( 1  /  n
) )  =  ( y ( ball `  D
) ( 1  /  n ) ) ) )
67 oveq1 5949 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  t  ->  (
y ( ball `  D
) ( 1  /  n ) )  =  ( t ( ball `  D ) ( 1  /  n ) ) )
6867eqeq2d 2369 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  t  ->  (
( t ( ball `  D ) ( 1  /  n ) )  =  ( y (
ball `  D )
( 1  /  n
) )  <->  ( t
( ball `  D )
( 1  /  n
) )  =  ( t ( ball `  D
) ( 1  /  n ) ) ) )
6966, 68rspc2ev 2968 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  /\  t  e.  A  /\  ( t ( ball `  D ) ( 1  /  n ) )  =  ( t (
ball `  D )
( 1  /  n
) ) )  ->  E. x  e.  NN  E. y  e.  A  ( t ( ball `  D
) ( 1  /  n ) )  =  ( y ( ball `  D ) ( 1  /  x ) ) )
7059, 62, 63, 69syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  E. x  e.  NN  E. y  e.  A  ( t ( ball `  D
) ( 1  /  n ) )  =  ( y ( ball `  D ) ( 1  /  x ) ) )
71 ovex 5967 . . . . . . . . . . . . . . . . 17  |-  ( t ( ball `  D
) ( 1  /  n ) )  e. 
_V
72 eqeq1 2364 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( t (
ball `  D )
( 1  /  n
) )  ->  (
z  =  ( y ( ball `  D
) ( 1  /  x ) )  <->  ( t
( ball `  D )
( 1  /  n
) )  =  ( y ( ball `  D
) ( 1  /  x ) ) ) )
73722rexbidv 2662 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( t (
ball `  D )
( 1  /  n
) )  ->  ( E. x  e.  NN  E. y  e.  A  z  =  ( y (
ball `  D )
( 1  /  x
) )  <->  E. x  e.  NN  E. y  e.  A  ( t (
ball `  D )
( 1  /  n
) )  =  ( y ( ball `  D
) ( 1  /  x ) ) ) )
7415rnmpt2 6038 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  NN , 
y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) )  =  { z  |  E. x  e.  NN  E. y  e.  A  z  =  ( y (
ball `  D )
( 1  /  x
) ) }
7571, 73, 74elab2 2993 . . . . . . . . . . . . . . . 16  |-  ( ( t ( ball `  D
) ( 1  /  n ) )  e. 
ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) )  <->  E. x  e.  NN  E. y  e.  A  ( t (
ball `  D )
( 1  /  n
) )  =  ( y ( ball `  D
) ( 1  /  x ) ) )
7670, 75sylibr 203 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t (
ball `  D )
( 1  /  n
) )  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) )
77 inss1 3465 . . . . . . . . . . . . . . . . 17  |-  ( ( z ( ball `  D
) ( 1  /  n ) )  i^i 
A )  C_  (
z ( ball `  D
) ( 1  /  n ) )
7877, 61sseldi 3254 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  t  e.  ( z ( ball `  D
) ( 1  /  n ) ) )
7945adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  D  e.  ( * Met `  X
) )
8049adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( 1  /  n )  e.  RR* )
8141adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  z  e.  X
)
8233adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  A  C_  X
)
8382, 62sseldd 3257 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  t  e.  X
)
84 blcom 18048 . . . . . . . . . . . . . . . . 17  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( 1  /  n )  e. 
RR* )  /\  (
z  e.  X  /\  t  e.  X )
)  ->  ( t  e.  ( z ( ball `  D ) ( 1  /  n ) )  <-> 
z  e.  ( t ( ball `  D
) ( 1  /  n ) ) ) )
8579, 80, 81, 83, 84syl22anc 1183 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t  e.  ( z ( ball `  D ) ( 1  /  n ) )  <-> 
z  e.  ( t ( ball `  D
) ( 1  /  n ) ) ) )
8678, 85mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  z  e.  ( t ( ball `  D
) ( 1  /  n ) ) )
87 simprll 738 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  r  e.  RR+ )
8887adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  r  e.  RR+ )
8988rphalfcld 10491 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( r  / 
2 )  e.  RR+ )
9089rpxrd 10480 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( r  / 
2 )  e.  RR* )
91 simprrr 741 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( 1  /  n )  <  (
r  /  2 ) )
9287rphalfcld 10491 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( r  / 
2 )  e.  RR+ )
93 rpre 10449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  /  n )  e.  RR+  ->  ( 1  /  n )  e.  RR )
94 rpre 10449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( r  /  2 )  e.  RR+  ->  ( r  /  2 )  e.  RR )
95 ltle 8997 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1  /  n
)  e.  RR  /\  ( r  /  2
)  e.  RR )  ->  ( ( 1  /  n )  < 
( r  /  2
)  ->  ( 1  /  n )  <_ 
( r  /  2
) ) )
9693, 94, 95syl2an 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  /  n
)  e.  RR+  /\  (
r  /  2 )  e.  RR+ )  ->  (
( 1  /  n
)  <  ( r  /  2 )  -> 
( 1  /  n
)  <_  ( r  /  2 ) ) )
9748, 92, 96syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( ( 1  /  n )  < 
( r  /  2
)  ->  ( 1  /  n )  <_ 
( r  /  2
) ) )
9891, 97mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( 1  /  n )  <_  (
r  /  2 ) )
9998adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( 1  /  n )  <_  (
r  /  2 ) )
100 ssbl 18067 . . . . . . . . . . . . . . . . 17  |-  ( ( ( D  e.  ( * Met `  X
)  /\  t  e.  X )  /\  (
( 1  /  n
)  e.  RR*  /\  (
r  /  2 )  e.  RR* )  /\  (
1  /  n )  <_  ( r  / 
2 ) )  -> 
( t ( ball `  D ) ( 1  /  n ) ) 
C_  ( t (
ball `  D )
( r  /  2
) ) )
10179, 83, 80, 90, 99, 100syl221anc 1193 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t (
ball `  D )
( 1  /  n
) )  C_  (
t ( ball `  D
) ( r  / 
2 ) ) )
10288rpred 10479 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  r  e.  RR )
103101, 86sseldd 3257 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  z  e.  ( t ( ball `  D
) ( r  / 
2 ) ) )
104 blhalf 18056 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( D  e.  ( * Met `  X
)  /\  t  e.  X )  /\  (
r  e.  RR  /\  z  e.  ( t
( ball `  D )
( r  /  2
) ) ) )  ->  ( t (
ball `  D )
( r  /  2
) )  C_  (
z ( ball `  D
) r ) )
10579, 83, 102, 103, 104syl22anc 1183 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t (
ball `  D )
( r  /  2
) )  C_  (
z ( ball `  D
) r ) )
106 simprlr 739 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( z (
ball `  D )
r )  C_  u
)
107106adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( z (
ball `  D )
r )  C_  u
)
108105, 107sstrd 3265 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t (
ball `  D )
( r  /  2
) )  C_  u
)
109101, 108sstrd 3265 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  ( t (
ball `  D )
( 1  /  n
) )  C_  u
)
110 eleq2 2419 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( t (
ball `  D )
( 1  /  n
) )  ->  (
z  e.  w  <->  z  e.  ( t ( ball `  D ) ( 1  /  n ) ) ) )
111 sseq1 3275 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( t (
ball `  D )
( 1  /  n
) )  ->  (
w  C_  u  <->  ( t
( ball `  D )
( 1  /  n
) )  C_  u
) )
112110, 111anbi12d 691 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( t (
ball `  D )
( 1  /  n
) )  ->  (
( z  e.  w  /\  w  C_  u )  <-> 
( z  e.  ( t ( ball `  D
) ( 1  /  n ) )  /\  ( t ( ball `  D ) ( 1  /  n ) ) 
C_  u ) ) )
113112rspcev 2960 . . . . . . . . . . . . . . 15  |-  ( ( ( t ( ball `  D ) ( 1  /  n ) )  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) )  /\  ( z  e.  ( t ( ball `  D ) ( 1  /  n ) )  /\  ( t (
ball `  D )
( 1  /  n
) )  C_  u
) )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) ( z  e.  w  /\  w  C_  u ) )
11476, 86, 109, 113syl12anc 1180 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  /\  t  e.  ( ( z ( ball `  D ) ( 1  /  n ) )  i^i  A ) )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )
115114ex 423 . . . . . . . . . . . . 13  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( t  e.  ( ( z (
ball `  D )
( 1  /  n
) )  i^i  A
)  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) ( z  e.  w  /\  w  C_  u ) ) )
116115exlimdv 1636 . . . . . . . . . . . 12  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  ( E. t 
t  e.  ( ( z ( ball `  D
) ( 1  /  n ) )  i^i 
A )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) ( z  e.  w  /\  w  C_  u ) ) )
11758, 116mpd 14 . . . . . . . . . . 11  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( ( r  e.  RR+  /\  ( z (
ball `  D )
r )  C_  u
)  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) ) )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )
118117anassrs 629 . . . . . . . . . 10  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( r  /  2
) ) )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )
119118expr 598 . . . . . . . . 9  |-  ( ( ( ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  /\  n  e.  NN )  ->  ( ( 1  /  n )  < 
( r  /  2
)  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) ( z  e.  w  /\  w  C_  u ) ) )
120119rexlimdva 2743 . . . . . . . 8  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  ->  ( E. n  e.  NN  ( 1  /  n )  <  (
r  /  2 )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) ) )
12130, 120mpd 14 . . . . . . 7  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  ( r  e.  RR+  /\  ( z ( ball `  D ) r ) 
C_  u ) )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )
122121expr 598 . . . . . 6  |-  ( ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  /\  r  e.  RR+ )  -> 
( ( z (
ball `  D )
r )  C_  u  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) ) )
123122rexlimdva 2743 . . . . 5  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  -> 
( E. r  e.  RR+  ( z ( ball `  D ) r ) 
C_  u  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) ( z  e.  w  /\  w  C_  u ) ) )
12424, 123mpd 14 . . . 4  |-  ( ( ( D  e.  ( * Met `  X
)  /\  ( A  C_  X  /\  A  ~<_  om 
/\  ( ( cls `  J ) `  A
)  =  X ) )  /\  ( u  e.  J  /\  z  e.  u ) )  ->  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )
125124ralrimivva 2711 . . 3  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  A. u  e.  J  A. z  e.  u  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )
126 basgen2 16827 . . 3  |-  ( ( J  e.  Top  /\  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  C_  J  /\  A. u  e.  J  A. z  e.  u  E. w  e.  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) ( z  e.  w  /\  w  C_  u ) )  ->  ( topGen ` 
ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) )  =  J )
1273, 19, 125, 126syl3anc 1182 . 2  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( topGen `  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) )  =  J )
128127, 3eqeltrd 2432 . . . 4  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( topGen `  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) )  e.  Top )
129 tgclb 16808 . . . 4  |-  ( ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  e.  TopBases  <->  ( topGen ` 
ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) )  e.  Top )
130128, 129sylibr 203 . . 3  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  e.  TopBases )
131 omelon 7434 . . . . . 6  |-  om  e.  On
132 simpr2 962 . . . . . . . 8  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  A  ~<_  om )
133 nnex 9839 . . . . . . . . 9  |-  NN  e.  _V
134133xpdom2 7042 . . . . . . . 8  |-  ( A  ~<_  om  ->  ( NN  X.  A )  ~<_  ( NN 
X.  om ) )
135132, 134syl 15 . . . . . . 7  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( NN  X.  A
)  ~<_  ( NN  X.  om ) )
136 nnenom 11131 . . . . . . . . 9  |-  NN  ~~  om
137 omex 7431 . . . . . . . . . 10  |-  om  e.  _V
138137enref 6979 . . . . . . . . 9  |-  om  ~~  om
139 xpen 7109 . . . . . . . . 9  |-  ( ( NN  ~~  om  /\  om 
~~  om )  ->  ( NN  X.  om )  ~~  ( om  X.  om )
)
140136, 138, 139mp2an 653 . . . . . . . 8  |-  ( NN 
X.  om )  ~~  ( om  X.  om )
141 xpomen 7730 . . . . . . . 8  |-  ( om 
X.  om )  ~~  om
142140, 141entri 7000 . . . . . . 7  |-  ( NN 
X.  om )  ~~  om
143 domentr 7005 . . . . . . 7  |-  ( ( ( NN  X.  A
)  ~<_  ( NN  X.  om )  /\  ( NN  X.  om )  ~~  om )  ->  ( NN  X.  A )  ~<_  om )
144135, 142, 143sylancl 643 . . . . . 6  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( NN  X.  A
)  ~<_  om )
145 ondomen 7751 . . . . . 6  |-  ( ( om  e.  On  /\  ( NN  X.  A
)  ~<_  om )  ->  ( NN  X.  A )  e. 
dom  card )
146131, 144, 145sylancr 644 . . . . 5  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( NN  X.  A
)  e.  dom  card )
147 ffn 5469 . . . . . . 7  |-  ( ( x  e.  NN , 
y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) : ( NN  X.  A ) --> J  -> 
( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  Fn  ( NN 
X.  A ) )
14817, 147syl 15 . . . . . 6  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  Fn  ( NN 
X.  A ) )
149 dffn4 5537 . . . . . 6  |-  ( ( x  e.  NN , 
y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) )  Fn  ( NN  X.  A )  <->  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) : ( NN  X.  A
) -onto-> ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) )
150148, 149sylib 188 . . . . 5  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) : ( NN 
X.  A ) -onto-> ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) )
151 fodomnum 7771 . . . . 5  |-  ( ( NN  X.  A )  e.  dom  card  ->  ( ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) ) : ( NN 
X.  A ) -onto-> ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) )  ~<_  ( NN  X.  A
) ) )
152146, 150, 151sylc 56 . . . 4  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  ~<_  ( NN  X.  A ) )
153 domtr 6999 . . . 4  |-  ( ( ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) )  ~<_  ( NN  X.  A )  /\  ( NN  X.  A )  ~<_  om )  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) )  ~<_  om )
154152, 144, 153syl2anc 642 . . 3  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D ) ( 1  /  x ) ) )  ~<_  om )
155 2ndci 17274 . . 3  |-  ( ( ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) )  e.  TopBases 
/\  ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) )  ~<_  om )  ->  ( topGen ` 
ran  ( x  e.  NN ,  y  e.  A  |->  ( y (
ball `  D )
( 1  /  x
) ) ) )  e.  2ndc )
156130, 154, 155syl2anc 642 . 2  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  -> 
( topGen `  ran  ( x  e.  NN ,  y  e.  A  |->  ( y ( ball `  D
) ( 1  /  x ) ) ) )  e.  2ndc )
157127, 156eqeltrrd 2433 1  |-  ( ( D  e.  ( * Met `  X )  /\  ( A  C_  X  /\  A  ~<_  om  /\  ( ( cls `  J
) `  A )  =  X ) )  ->  J  e.  2ndc )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934   E.wex 1541    = wceq 1642    e. wcel 1710    =/= wne 2521   A.wral 2619   E.wrex 2620    i^i cin 3227    C_ wss 3228   (/)c0 3531   U.cuni 3906   class class class wbr 4102   Oncon0 4471   omcom 4735    X. cxp 4766   dom cdm 4768   ran crn 4769    Fn wfn 5329   -->wf 5330   -onto->wfo 5332   ` cfv 5334  (class class class)co 5942    e. cmpt2 5944    ~~ cen 6945    ~<_ cdom 6946   cardccrd 7655   RRcr 8823   0cc0 8824   1c1 8825   RR*cxr 8953    < clt 8954    <_ cle 8955    / cdiv 9510   NNcn 9833   2c2 9882   RR+crp 10443   topGenctg 13435   * Metcxmt 16462   ballcbl 16464   MetOpencmopn 16467   Topctop 16731   TopBasesctb 16735   clsccl 16855   2ndcc2ndc 17264
This theorem is referenced by:  met2ndc  18165
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-inf2 7429  ax-cnex 8880  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900  ax-pre-mulgt0 8901  ax-pre-sup 8902
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-iin 3987  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-se 4432  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-isom 5343  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-1st 6206  df-2nd 6207  df-riota 6388  df-recs 6472  df-rdg 6507  df-1o 6563  df-oadd 6567  df-er 6744  df-map 6859  df-en 6949  df-dom 6950  df-sdom 6951  df-fin 6952  df-sup 7281  df-oi 7312  df-card 7659  df-acn 7662  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-sub 9126  df-neg 9127  df-div 9511  df-nn 9834  df-2 9891  df-n0 10055  df-z 10114  df-uz 10320  df-q 10406  df-rp 10444  df-xneg 10541  df-xadd 10542  df-xmul 10543  df-topgen 13437  df-xmet 16469  df-bl 16471  df-mopn 16472  df-top 16736  df-bases 16738  df-topon 16739  df-cld 16856  df-ntr 16857  df-cls 16858  df-2ndc 17266
  Copyright terms: Public domain W3C validator