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

Theorem ubthlem1 21374
Description: Lemma for ubth 21377. The function  A exhibits a countable collection of sets that are closed, being the inverse image under  t of the closed ball of radius  k, and by assumption they cover  X. Thus by the Baire Category theorem bcth2 18679, for some  n the set  A `  n has an interior, meaning that there is a closed ball  { z  e.  X  |  ( y D z )  <_  r } in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
ubth.1  |-  X  =  ( BaseSet `  U )
ubth.2  |-  N  =  ( normCV `  W )
ubthlem.3  |-  D  =  ( IndMet `  U )
ubthlem.4  |-  J  =  ( MetOpen `  D )
ubthlem.5  |-  U  e. 
CBan
ubthlem.6  |-  W  e.  NrmCVec
ubthlem.7  |-  ( ph  ->  T  C_  ( U  BLnOp  W ) )
ubthlem.8  |-  ( ph  ->  A. x  e.  X  E. c  e.  RR  A. t  e.  T  ( N `  ( t `
 x ) )  <_  c )
ubthlem.9  |-  A  =  ( k  e.  NN  |->  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
Assertion
Ref Expression
ubthlem1  |-  ( ph  ->  E. n  e.  NN  E. y  e.  X  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) )
Distinct variable groups:    k, c, n, r, x, y, z, A    t, c, D, k, n, r, x, z    k, J, n   
y, t, J, x    N, c, k, n, r, t, x, y, z    ph, c, k, n, r, t, x, y    T, c, k, n, r, t, x, y, z    U, c, n, r, t, x, y, z    W, c, n, r, t, x, y    X, c, k, n, r, t, x, y, z
Allowed substitution hints:    ph( z)    A( t)    D( y)    U( k)    J( z, r, c)    W( z, k)

Proof of Theorem ubthlem1
StepHypRef Expression
1 rzal 3497 . . . . . . . . 9  |-  ( T  =  (/)  ->  A. t  e.  T  ( N `  ( t `  z
) )  <_  k
)
21ralrimivw 2598 . . . . . . . 8  |-  ( T  =  (/)  ->  A. z  e.  X  A. t  e.  T  ( N `  ( t `  z
) )  <_  k
)
3 rabid2 2685 . . . . . . . 8  |-  ( X  =  { z  e.  X  |  A. t  e.  T  ( N `  ( t `  z
) )  <_  k } 
<-> 
A. z  e.  X  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k )
42, 3sylibr 205 . . . . . . 7  |-  ( T  =  (/)  ->  X  =  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
54eqcomd 2261 . . . . . 6  |-  ( T  =  (/)  ->  { z  e.  X  |  A. t  e.  T  ( N `  ( t `  z ) )  <_ 
k }  =  X )
65eleq1d 2322 . . . . 5  |-  ( T  =  (/)  ->  ( { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k }  e.  ( Clsd `  J )  <->  X  e.  ( Clsd `  J
) ) )
7 iinrab 3905 . . . . . . 7  |-  ( T  =/=  (/)  ->  |^|_ t  e.  T  { z  e.  X  |  ( N `
 ( t `  z ) )  <_ 
k }  =  {
z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
87adantl 454 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  T  =/=  (/) )  ->  |^|_ t  e.  T  { z  e.  X  |  ( N `  ( t `  z ) )  <_ 
k }  =  {
z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
9 id 21 . . . . . . 7  |-  ( T  =/=  (/)  ->  T  =/=  (/) )
10 ubthlem.7 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  C_  ( U  BLnOp  W ) )
1110sselda 3122 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  ( U  BLnOp  W ) )
12 ubthlem.3 . . . . . . . . . . . . . . . . . . . 20  |-  D  =  ( IndMet `  U )
13 eqid 2256 . . . . . . . . . . . . . . . . . . . 20  |-  ( IndMet `  W )  =  (
IndMet `  W )
14 ubthlem.4 . . . . . . . . . . . . . . . . . . . 20  |-  J  =  ( MetOpen `  D )
15 eqid 2256 . . . . . . . . . . . . . . . . . . . 20  |-  ( MetOpen `  ( IndMet `  W )
)  =  ( MetOpen `  ( IndMet `  W )
)
16 eqid 2256 . . . . . . . . . . . . . . . . . . . 20  |-  ( U 
BLnOp  W )  =  ( U  BLnOp  W )
17 ubthlem.5 . . . . . . . . . . . . . . . . . . . . 21  |-  U  e. 
CBan
18 bnnv 21370 . . . . . . . . . . . . . . . . . . . . 21  |-  ( U  e.  CBan  ->  U  e.  NrmCVec )
1917, 18ax-mp 10 . . . . . . . . . . . . . . . . . . . 20  |-  U  e.  NrmCVec
20 ubthlem.6 . . . . . . . . . . . . . . . . . . . 20  |-  W  e.  NrmCVec
2112, 13, 14, 15, 16, 19, 20blocn2 21311 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( U  BLnOp  W )  ->  t  e.  ( J  Cn  ( MetOpen
`  ( IndMet `  W
) ) ) )
22 ubth.1 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  X  =  ( BaseSet `  U )
2322, 12cbncms 21369 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U  e.  CBan  ->  D  e.  ( CMet `  X
) )
2417, 23ax-mp 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  D  e.  ( CMet `  X
)
25 cmetmet 18639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  e.  ( CMet `  X
)  ->  D  e.  ( Met `  X ) )
26 metxmet 17826 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( * Met `  X
) )
2724, 25, 26mp2b 11 . . . . . . . . . . . . . . . . . . . . 21  |-  D  e.  ( * Met `  X
)
2814mopntopon 17912 . . . . . . . . . . . . . . . . . . . . 21  |-  ( D  e.  ( * Met `  X )  ->  J  e.  (TopOn `  X )
)
2927, 28ax-mp 10 . . . . . . . . . . . . . . . . . . . 20  |-  J  e.  (TopOn `  X )
30 eqid 2256 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( BaseSet `  W )  =  (
BaseSet `  W )
3130, 13imsxmet 21186 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( W  e.  NrmCVec  ->  ( IndMet `  W
)  e.  ( * Met `  ( BaseSet `  W ) ) )
3220, 31ax-mp 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( IndMet `  W )  e.  ( * Met `  ( BaseSet
`  W ) )
3315mopntopon 17912 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
IndMet `  W )  e.  ( * Met `  ( BaseSet
`  W ) )  ->  ( MetOpen `  ( IndMet `
 W ) )  e.  (TopOn `  ( BaseSet
`  W ) ) )
3432, 33ax-mp 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( MetOpen `  ( IndMet `  W )
)  e.  (TopOn `  ( BaseSet `  W )
)
35 iscncl 16925 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( J  e.  (TopOn `  X )  /\  ( MetOpen
`  ( IndMet `  W
) )  e.  (TopOn `  ( BaseSet `  W )
) )  ->  (
t  e.  ( J  Cn  ( MetOpen `  ( IndMet `
 W ) ) )  <->  ( t : X --> ( BaseSet `  W
)  /\  A. x  e.  ( Clsd `  ( MetOpen
`  ( IndMet `  W
) ) ) ( `' t " x
)  e.  ( Clsd `  J ) ) ) )
3629, 34, 35mp2an 656 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( J  Cn  ( MetOpen `  ( IndMet `  W ) ) )  <-> 
( t : X --> ( BaseSet `  W )  /\  A. x  e.  (
Clsd `  ( MetOpen `  ( IndMet `
 W ) ) ) ( `' t
" x )  e.  ( Clsd `  J
) ) )
3721, 36sylib 190 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( U  BLnOp  W )  ->  ( t : X --> ( BaseSet `  W
)  /\  A. x  e.  ( Clsd `  ( MetOpen
`  ( IndMet `  W
) ) ) ( `' t " x
)  e.  ( Clsd `  J ) ) )
3811, 37syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
t : X --> ( BaseSet `  W )  /\  A. x  e.  ( Clsd `  ( MetOpen `  ( IndMet `  W ) ) ) ( `' t "
x )  e.  (
Clsd `  J )
) )
3938simpld 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  t : X --> ( BaseSet `  W
) )
4039adantlr 698 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  t : X --> ( BaseSet `  W
) )
41 ffvelrn 5562 . . . . . . . . . . . . . . 15  |-  ( ( t : X --> ( BaseSet `  W )  /\  x  e.  X )  ->  (
t `  x )  e.  ( BaseSet `  W )
)
4240, 41sylan 459 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T
)  /\  x  e.  X )  ->  (
t `  x )  e.  ( BaseSet `  W )
)
4342biantrurd 496 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T
)  /\  x  e.  X )  ->  (
( N `  (
t `  x )
)  <_  k  <->  ( (
t `  x )  e.  ( BaseSet `  W )  /\  ( N `  (
t `  x )
)  <_  k )
) )
44 fveq2 5423 . . . . . . . . . . . . . . 15  |-  ( y  =  ( t `  x )  ->  ( N `  y )  =  ( N `  ( t `  x
) ) )
4544breq1d 3973 . . . . . . . . . . . . . 14  |-  ( y  =  ( t `  x )  ->  (
( N `  y
)  <_  k  <->  ( N `  ( t `  x
) )  <_  k
) )
4645elrab 2874 . . . . . . . . . . . . 13  |-  ( ( t `  x )  e.  { y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k } 
<->  ( ( t `  x )  e.  (
BaseSet `  W )  /\  ( N `  ( t `
 x ) )  <_  k ) )
4743, 46syl6bbr 256 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T
)  /\  x  e.  X )  ->  (
( N `  (
t `  x )
)  <_  k  <->  ( t `  x )  e.  {
y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k } ) )
4847pm5.32da 625 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  (
( x  e.  X  /\  ( N `  (
t `  x )
)  <_  k )  <->  ( x  e.  X  /\  ( t `  x
)  e.  { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k } ) ) )
49 fveq2 5423 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  (
t `  z )  =  ( t `  x ) )
5049fveq2d 5427 . . . . . . . . . . . . . 14  |-  ( z  =  x  ->  ( N `  ( t `  z ) )  =  ( N `  (
t `  x )
) )
5150breq1d 3973 . . . . . . . . . . . . 13  |-  ( z  =  x  ->  (
( N `  (
t `  z )
)  <_  k  <->  ( N `  ( t `  x
) )  <_  k
) )
5251elrab 2874 . . . . . . . . . . . 12  |-  ( x  e.  { z  e.  X  |  ( N `
 ( t `  z ) )  <_ 
k }  <->  ( x  e.  X  /\  ( N `  ( t `  x ) )  <_ 
k ) )
5352a1i 12 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  (
x  e.  { z  e.  X  |  ( N `  ( t `
 z ) )  <_  k }  <->  ( x  e.  X  /\  ( N `  ( t `  x ) )  <_ 
k ) ) )
54 ffn 5292 . . . . . . . . . . . 12  |-  ( t : X --> ( BaseSet `  W )  ->  t  Fn  X )
55 elpreima 5544 . . . . . . . . . . . 12  |-  ( t  Fn  X  ->  (
x  e.  ( `' t " { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k } )  <->  ( x  e.  X  /\  (
t `  x )  e.  { y  e.  (
BaseSet `  W )  |  ( N `  y
)  <_  k }
) ) )
5640, 54, 553syl 20 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  (
x  e.  ( `' t " { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k } )  <->  ( x  e.  X  /\  (
t `  x )  e.  { y  e.  (
BaseSet `  W )  |  ( N `  y
)  <_  k }
) ) )
5748, 53, 563bitr4d 278 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  (
x  e.  { z  e.  X  |  ( N `  ( t `
 z ) )  <_  k }  <->  x  e.  ( `' t " {
y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k } ) ) )
5857eqrdv 2254 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  { z  e.  X  |  ( N `  ( t `
 z ) )  <_  k }  =  ( `' t " {
y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k } ) )
59 nnre 9686 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  RR )
6059ad2antlr 710 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  k  e.  RR )
6160rexrd 8814 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  k  e.  RR* )
62 eqid 2256 . . . . . . . . . . . . . 14  |-  ( 0vec `  W )  =  (
0vec `  W )
6330, 62nvzcl 21117 . . . . . . . . . . . . 13  |-  ( W  e.  NrmCVec  ->  ( 0vec `  W
)  e.  ( BaseSet `  W ) )
6420, 63ax-mp 10 . . . . . . . . . . . 12  |-  ( 0vec `  W )  e.  (
BaseSet `  W )
65 ubth.2 . . . . . . . . . . . . . . . . . 18  |-  N  =  ( normCV `  W )
6630, 62, 65, 13nvnd 21182 . . . . . . . . . . . . . . . . 17  |-  ( ( W  e.  NrmCVec  /\  y  e.  ( BaseSet `  W )
)  ->  ( N `  y )  =  ( y ( IndMet `  W
) ( 0vec `  W
) ) )
6720, 66mpan 654 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( BaseSet `  W
)  ->  ( N `  y )  =  ( y ( IndMet `  W
) ( 0vec `  W
) ) )
68 xmetsym 17839 . . . . . . . . . . . . . . . . 17  |-  ( ( ( IndMet `  W )  e.  ( * Met `  ( BaseSet
`  W ) )  /\  ( 0vec `  W
)  e.  ( BaseSet `  W )  /\  y  e.  ( BaseSet `  W )
)  ->  ( ( 0vec `  W ) (
IndMet `  W ) y )  =  ( y ( IndMet `  W )
( 0vec `  W )
) )
6932, 64, 68mp3an12 1272 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( BaseSet `  W
)  ->  ( ( 0vec `  W ) (
IndMet `  W ) y )  =  ( y ( IndMet `  W )
( 0vec `  W )
) )
7067, 69eqtr4d 2291 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( BaseSet `  W
)  ->  ( N `  y )  =  ( ( 0vec `  W
) ( IndMet `  W
) y ) )
7170breq1d 3973 . . . . . . . . . . . . . 14  |-  ( y  e.  ( BaseSet `  W
)  ->  ( ( N `  y )  <_  k  <->  ( ( 0vec `  W ) ( IndMet `  W ) y )  <_  k ) )
7271rabbiia 2730 . . . . . . . . . . . . 13  |-  { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k }  =  {
y  e.  ( BaseSet `  W )  |  ( ( 0vec `  W
) ( IndMet `  W
) y )  <_ 
k }
7315, 72blcld 17978 . . . . . . . . . . . 12  |-  ( ( ( IndMet `  W )  e.  ( * Met `  ( BaseSet
`  W ) )  /\  ( 0vec `  W
)  e.  ( BaseSet `  W )  /\  k  e.  RR* )  ->  { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k }  e.  (
Clsd `  ( MetOpen `  ( IndMet `
 W ) ) ) )
7432, 64, 73mp3an12 1272 . . . . . . . . . . 11  |-  ( k  e.  RR*  ->  { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k }  e.  (
Clsd `  ( MetOpen `  ( IndMet `
 W ) ) ) )
7561, 74syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  { y  e.  ( BaseSet `  W
)  |  ( N `
 y )  <_ 
k }  e.  (
Clsd `  ( MetOpen `  ( IndMet `
 W ) ) ) )
7638simprd 451 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  A. x  e.  ( Clsd `  ( MetOpen
`  ( IndMet `  W
) ) ) ( `' t " x
)  e.  ( Clsd `  J ) )
7776adantlr 698 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  A. x  e.  ( Clsd `  ( MetOpen
`  ( IndMet `  W
) ) ) ( `' t " x
)  e.  ( Clsd `  J ) )
78 imaeq2 4961 . . . . . . . . . . . 12  |-  ( x  =  { y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k }  ->  ( `' t
" x )  =  ( `' t " { y  e.  (
BaseSet `  W )  |  ( N `  y
)  <_  k }
) )
7978eleq1d 2322 . . . . . . . . . . 11  |-  ( x  =  { y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k }  ->  ( ( `' t " x )  e.  ( Clsd `  J
)  <->  ( `' t
" { y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k } )  e.  (
Clsd `  J )
) )
8079rcla4v 2831 . . . . . . . . . 10  |-  ( { y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k }  e.  ( Clsd `  ( MetOpen `  ( IndMet `
 W ) ) )  ->  ( A. x  e.  ( Clsd `  ( MetOpen `  ( IndMet `  W ) ) ) ( `' t "
x )  e.  (
Clsd `  J )  ->  ( `' t " { y  e.  (
BaseSet `  W )  |  ( N `  y
)  <_  k }
)  e.  ( Clsd `  J ) ) )
8175, 77, 80sylc 58 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  ( `' t " {
y  e.  ( BaseSet `  W )  |  ( N `  y )  <_  k } )  e.  ( Clsd `  J
) )
8258, 81eqeltrd 2330 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  t  e.  T )  ->  { z  e.  X  |  ( N `  ( t `
 z ) )  <_  k }  e.  ( Clsd `  J )
)
8382ralrimiva 2597 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  A. t  e.  T  { z  e.  X  |  ( N `  ( t `  z ) )  <_ 
k }  e.  (
Clsd `  J )
)
84 iincld 16703 . . . . . . 7  |-  ( ( T  =/=  (/)  /\  A. t  e.  T  {
z  e.  X  | 
( N `  (
t `  z )
)  <_  k }  e.  ( Clsd `  J
) )  ->  |^|_ t  e.  T  { z  e.  X  |  ( N `  ( t `  z ) )  <_ 
k }  e.  (
Clsd `  J )
)
859, 83, 84syl2anr 466 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  T  =/=  (/) )  ->  |^|_ t  e.  T  { z  e.  X  |  ( N `  ( t `  z ) )  <_ 
k }  e.  (
Clsd `  J )
)
868, 85eqeltrrd 2331 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  T  =/=  (/) )  ->  { z  e.  X  |  A. t  e.  T  ( N `  ( t `  z ) )  <_ 
k }  e.  (
Clsd `  J )
)
8714mopntop 17913 . . . . . . . 8  |-  ( D  e.  ( * Met `  X )  ->  J  e.  Top )
8827, 87ax-mp 10 . . . . . . 7  |-  J  e. 
Top
8929toponunii 16597 . . . . . . . 8  |-  X  = 
U. J
9089topcld 16699 . . . . . . 7  |-  ( J  e.  Top  ->  X  e.  ( Clsd `  J
) )
9188, 90ax-mp 10 . . . . . 6  |-  X  e.  ( Clsd `  J
)
9291a1i 12 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  ( Clsd `  J
) )
936, 86, 92pm2.61ne 2494 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  { z  e.  X  |  A. t  e.  T  ( N `  ( t `  z ) )  <_ 
k }  e.  (
Clsd `  J )
)
94 ubthlem.9 . . . 4  |-  A  =  ( k  e.  NN  |->  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
9593, 94fmptd 5583 . . 3  |-  ( ph  ->  A : NN --> ( Clsd `  J ) )
96 frn 5298 . . . . . . 7  |-  ( A : NN --> ( Clsd `  J )  ->  ran  A 
C_  ( Clsd `  J
) )
9795, 96syl 17 . . . . . 6  |-  ( ph  ->  ran  A  C_  ( Clsd `  J ) )
9889cldss2 16694 . . . . . 6  |-  ( Clsd `  J )  C_  ~P X
9997, 98syl6ss 3133 . . . . 5  |-  ( ph  ->  ran  A  C_  ~P X )
100 sspwuni 3928 . . . . 5  |-  ( ran 
A  C_  ~P X  <->  U.
ran  A  C_  X )
10199, 100sylib 190 . . . 4  |-  ( ph  ->  U. ran  A  C_  X )
102 ubthlem.8 . . . . . 6  |-  ( ph  ->  A. x  e.  X  E. c  e.  RR  A. t  e.  T  ( N `  ( t `
 x ) )  <_  c )
103 arch 9894 . . . . . . . . . 10  |-  ( c  e.  RR  ->  E. k  e.  NN  c  <  k
)
104103adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  ->  E. k  e.  NN  c  <  k
)
105 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  ->  c  e.  RR )
106 ltle 8843 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  RR  /\  k  e.  RR )  ->  ( c  <  k  ->  c  <_  k )
)
107105, 59, 106syl2an 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  k  e.  NN )  ->  ( c  < 
k  ->  c  <_  k ) )
108107impr 605 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  -> 
c  <_  k )
109108adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  c  <_  k )
11039, 41sylan 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  x  e.  X )  ->  (
t `  x )  e.  ( BaseSet `  W )
)
111110an32s 782 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  T )  ->  (
t `  x )  e.  ( BaseSet `  W )
)
11230, 65nvcl 21150 . . . . . . . . . . . . . . . . . 18  |-  ( ( W  e.  NrmCVec  /\  (
t `  x )  e.  ( BaseSet `  W )
)  ->  ( N `  ( t `  x
) )  e.  RR )
11320, 111, 112sylancr 647 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  t  e.  T )  ->  ( N `  ( t `  x ) )  e.  RR )
114113adantlr 698 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  t  e.  T
)  ->  ( N `  ( t `  x
) )  e.  RR )
115114adantlr 698 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  ( N `  (
t `  x )
)  e.  RR )
116 simpllr 738 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  c  e.  RR )
117 simplrl 739 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  k  e.  NN )
118117, 59syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  k  e.  RR )
119 letr 8847 . . . . . . . . . . . . . . 15  |-  ( ( ( N `  (
t `  x )
)  e.  RR  /\  c  e.  RR  /\  k  e.  RR )  ->  (
( ( N `  ( t `  x
) )  <_  c  /\  c  <_  k )  ->  ( N `  ( t `  x
) )  <_  k
) )
120115, 116, 118, 119syl3anc 1187 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  ( ( ( N `
 ( t `  x ) )  <_ 
c  /\  c  <_  k )  ->  ( N `  ( t `  x
) )  <_  k
) )
121109, 120mpan2d 658 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  /\  t  e.  T )  ->  ( ( N `  ( t `  x
) )  <_  c  ->  ( N `  (
t `  x )
)  <_  k )
)
122121ralimdva 2592 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  ( k  e.  NN  /\  c  < 
k ) )  -> 
( A. t  e.  T  ( N `  ( t `  x
) )  <_  c  ->  A. t  e.  T  ( N `  ( t `
 x ) )  <_  k ) )
123122expr 601 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  k  e.  NN )  ->  ( c  < 
k  ->  ( A. t  e.  T  ( N `  ( t `  x ) )  <_ 
c  ->  A. t  e.  T  ( N `  ( t `  x
) )  <_  k
) ) )
124 fvex 5437 . . . . . . . . . . . . . . . . . . 19  |-  ( BaseSet `  U )  e.  _V
12522, 124eqeltri 2326 . . . . . . . . . . . . . . . . . 18  |-  X  e. 
_V
126125rabex 4105 . . . . . . . . . . . . . . . . 17  |-  { z  e.  X  |  A. t  e.  T  ( N `  ( t `  z ) )  <_ 
k }  e.  _V
12794fvmpt2 5507 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN  /\  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k }  e.  _V )  ->  ( A `
 k )  =  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
128126, 127mpan2 655 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  ( A `  k )  =  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } )
129128eleq2d 2323 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
x  e.  ( A `
 k )  <->  x  e.  { z  e.  X  |  A. t  e.  T  ( N `  ( t `
 z ) )  <_  k } ) )
13051ralbidv 2534 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  ( A. t  e.  T  ( N `  ( t `
 z ) )  <_  k  <->  A. t  e.  T  ( N `  ( t `  x
) )  <_  k
) )
131130elrab 2874 . . . . . . . . . . . . . . 15  |-  ( x  e.  { z  e.  X  |  A. t  e.  T  ( N `  ( t `  z
) )  <_  k } 
<->  ( x  e.  X  /\  A. t  e.  T  ( N `  ( t `
 x ) )  <_  k ) )
132129, 131syl6bb 254 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  (
x  e.  ( A `
 k )  <->  ( x  e.  X  /\  A. t  e.  T  ( N `  ( t `  x
) )  <_  k
) ) )
133 simpr 449 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  X )  ->  x  e.  X )
134133biantrurd 496 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  X )  ->  ( A. t  e.  T  ( N `  ( t `
 x ) )  <_  k  <->  ( x  e.  X  /\  A. t  e.  T  ( N `  ( t `  x
) )  <_  k
) ) )
135134bicomd 194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  X )  ->  (
( x  e.  X  /\  A. t  e.  T  ( N `  ( t `
 x ) )  <_  k )  <->  A. t  e.  T  ( N `  ( t `  x
) )  <_  k
) )
136132, 135sylan9bbr 684 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  NN )  ->  (
x  e.  ( A `
 k )  <->  A. t  e.  T  ( N `  ( t `  x
) )  <_  k
) )
137 ffn 5292 . . . . . . . . . . . . . . . 16  |-  ( A : NN --> ( Clsd `  J )  ->  A  Fn  NN )
13895, 137syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  Fn  NN )
139138adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  X )  ->  A  Fn  NN )
140 fnfvelrn 5561 . . . . . . . . . . . . . . . 16  |-  ( ( A  Fn  NN  /\  k  e.  NN )  ->  ( A `  k
)  e.  ran  A
)
141 elssuni 3796 . . . . . . . . . . . . . . . 16  |-  ( ( A `  k )  e.  ran  A  -> 
( A `  k
)  C_  U. ran  A
)
142140, 141syl 17 . . . . . . . . . . . . . . 15  |-  ( ( A  Fn  NN  /\  k  e.  NN )  ->  ( A `  k
)  C_  U. ran  A
)
143142sseld 3121 . . . . . . . . . . . . . 14  |-  ( ( A  Fn  NN  /\  k  e.  NN )  ->  ( x  e.  ( A `  k )  ->  x  e.  U. ran  A ) )
144139, 143sylan 459 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  NN )  ->  (
x  e.  ( A `
 k )  ->  x  e.  U. ran  A
) )
145136, 144sylbird 228 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  NN )  ->  ( A. t  e.  T  ( N `  ( t `
 x ) )  <_  k  ->  x  e.  U. ran  A ) )
146145adantlr 698 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  k  e.  NN )  ->  ( A. t  e.  T  ( N `  ( t `  x
) )  <_  k  ->  x  e.  U. ran  A ) )
147123, 146syl6d 66 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  /\  k  e.  NN )  ->  ( c  < 
k  ->  ( A. t  e.  T  ( N `  ( t `  x ) )  <_ 
c  ->  x  e.  U.
ran  A ) ) )
148147rexlimdva 2638 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  ->  ( E. k  e.  NN  c  <  k  ->  ( A. t  e.  T  ( N `  ( t `
 x ) )  <_  c  ->  x  e.  U. ran  A ) ) )
149104, 148mpd 16 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  X )  /\  c  e.  RR )  ->  ( A. t  e.  T  ( N `  ( t `
 x ) )  <_  c  ->  x  e.  U. ran  A ) )
150149rexlimdva 2638 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  ( E. c  e.  RR  A. t  e.  T  ( N `  ( t `
 x ) )  <_  c  ->  x  e.  U. ran  A ) )
151150ralimdva 2592 . . . . . 6  |-  ( ph  ->  ( A. x  e.  X  E. c  e.  RR  A. t  e.  T  ( N `  ( t `  x
) )  <_  c  ->  A. x  e.  X  x  e.  U. ran  A
) )
152102, 151mpd 16 . . . . 5  |-  ( ph  ->  A. x  e.  X  x  e.  U. ran  A
)
153 dfss3 3112 . . . . 5  |-  ( X 
C_  U. ran  A  <->  A. x  e.  X  x  e.  U.
ran  A )
154152, 153sylibr 205 . . . 4  |-  ( ph  ->  X  C_  U. ran  A
)
155101, 154eqssd 3138 . . 3  |-  ( ph  ->  U. ran  A  =  X )
156 eqid 2256 . . . . . 6  |-  ( 0vec `  U )  =  (
0vec `  U )
15722, 156nvzcl 21117 . . . . 5  |-  ( U  e.  NrmCVec  ->  ( 0vec `  U
)  e.  X )
158 ne0i 3403 . . . . 5  |-  ( (
0vec `  U )  e.  X  ->  X  =/=  (/) )
15919, 157, 158mp2b 11 . . . 4  |-  X  =/=  (/)
16014bcth2 18679 . . . 4  |-  ( ( ( D  e.  (
CMet `  X )  /\  X  =/=  (/) )  /\  ( A : NN --> ( Clsd `  J )  /\  U. ran  A  =  X ) )  ->  E. n  e.  NN  ( ( int `  J ) `  ( A `  n )
)  =/=  (/) )
16124, 159, 160mpanl12 666 . . 3  |-  ( ( A : NN --> ( Clsd `  J )  /\  U. ran  A  =  X )  ->  E. n  e.  NN  ( ( int `  J
) `  ( A `  n ) )  =/=  (/) )
16295, 155, 161syl2anc 645 . 2  |-  ( ph  ->  E. n  e.  NN  ( ( int `  J
) `  ( A `  n ) )  =/=  (/) )
163 ffvelrn 5562 . . . . . . . . . . 11  |-  ( ( A : NN --> ( Clsd `  J )  /\  n  e.  NN )  ->  ( A `  n )  e.  ( Clsd `  J
) )
16498, 163sseldi 3120 . . . . . . . . . 10  |-  ( ( A : NN --> ( Clsd `  J )  /\  n  e.  NN )  ->  ( A `  n )  e.  ~P X )
165 elpwi 3574 . . . . . . . . . 10  |-  ( ( A `  n )  e.  ~P X  -> 
( A `  n
)  C_  X )
166164, 165syl 17 . . . . . . . . 9  |-  ( ( A : NN --> ( Clsd `  J )  /\  n  e.  NN )  ->  ( A `  n )  C_  X )
16795, 166sylan 459 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  X )
16889ntrss3 16724 . . . . . . . 8  |-  ( ( J  e.  Top  /\  ( A `  n ) 
C_  X )  -> 
( ( int `  J
) `  ( A `  n ) )  C_  X )
16988, 167, 168sylancr 647 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( int `  J ) `
 ( A `  n ) )  C_  X )
170169sseld 3121 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( y  e.  ( ( int `  J ) `  ( A `  n )
)  ->  y  e.  X ) )
17189ntropn 16713 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  ( A `  n ) 
C_  X )  -> 
( ( int `  J
) `  ( A `  n ) )  e.  J )
17288, 167, 171sylancr 647 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( int `  J ) `
 ( A `  n ) )  e.  J )
17314mopni2 17966 . . . . . . . . . 10  |-  ( ( D  e.  ( * Met `  X )  /\  ( ( int `  J ) `  ( A `  n )
)  e.  J  /\  y  e.  ( ( int `  J ) `  ( A `  n ) ) )  ->  E. x  e.  RR+  ( y (
ball `  D )
x )  C_  (
( int `  J
) `  ( A `  n ) ) )
17427, 173mp3an1 1269 . . . . . . . . 9  |-  ( ( ( ( int `  J
) `  ( A `  n ) )  e.  J  /\  y  e.  ( ( int `  J
) `  ( A `  n ) ) )  ->  E. x  e.  RR+  ( y ( ball `  D ) x ) 
C_  ( ( int `  J ) `  ( A `  n )
) )
175172, 174sylan 459 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( int `  J
) `  ( A `  n ) ) )  ->  E. x  e.  RR+  ( y ( ball `  D ) x ) 
C_  ( ( int `  J ) `  ( A `  n )
) )
176 elssuni 3796 . . . . . . . . . . . 12  |-  ( ( ( int `  J
) `  ( A `  n ) )  e.  J  ->  ( ( int `  J ) `  ( A `  n ) )  C_  U. J )
177176, 89syl6sseqr 3167 . . . . . . . . . . 11  |-  ( ( ( int `  J
) `  ( A `  n ) )  e.  J  ->  ( ( int `  J ) `  ( A `  n ) )  C_  X )
178172, 177syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( int `  J ) `
 ( A `  n ) )  C_  X )
179178sselda 3122 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( int `  J
) `  ( A `  n ) ) )  ->  y  e.  X
)
18089ntrss2 16721 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( A `  n ) 
C_  X )  -> 
( ( int `  J
) `  ( A `  n ) )  C_  ( A `  n ) )
18188, 167, 180sylancr 647 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( int `  J ) `
 ( A `  n ) )  C_  ( A `  n ) )
182 sstr2 3128 . . . . . . . . . . . . 13  |-  ( ( y ( ball `  D
) x )  C_  ( ( int `  J
) `  ( A `  n ) )  -> 
( ( ( int `  J ) `  ( A `  n )
)  C_  ( A `  n )  ->  (
y ( ball `  D
) x )  C_  ( A `  n ) ) )
183181, 182syl5com 28 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( y ( ball `  D
) x )  C_  ( ( int `  J
) `  ( A `  n ) )  -> 
( y ( ball `  D ) x ) 
C_  ( A `  n ) ) )
184183ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X
)  /\  x  e.  RR+ )  ->  ( (
y ( ball `  D
) x )  C_  ( ( int `  J
) `  ( A `  n ) )  -> 
( y ( ball `  D ) x ) 
C_  ( A `  n ) ) )
185 simpr 449 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X )  ->  y  e.  X )
186185, 27jctil 525 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X )  ->  ( D  e.  ( * Met `  X )  /\  y  e.  X )
)
187 rphalfcl 10310 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR+ )
188187rpxrd 10323 . . . . . . . . . . . . . 14  |-  ( x  e.  RR+  ->  ( x  /  2 )  e. 
RR* )
189 rpxr 10293 . . . . . . . . . . . . . 14  |-  ( x  e.  RR+  ->  x  e. 
RR* )
190 rphalflt 10312 . . . . . . . . . . . . . 14  |-  ( x  e.  RR+  ->  ( x  /  2 )  < 
x )
191188, 189, 1903jca 1137 . . . . . . . . . . . . 13  |-  ( x  e.  RR+  ->  ( ( x  /  2 )  e.  RR*  /\  x  e.  RR*  /\  ( x  /  2 )  < 
x ) )
192 eqid 2256 . . . . . . . . . . . . . 14  |-  { z  e.  X  |  ( y D z )  <_  ( x  / 
2 ) }  =  { z  e.  X  |  ( y D z )  <_  (
x  /  2 ) }
19314, 192blsscls2 17977 . . . . . . . . . . . . 13  |-  ( ( ( D  e.  ( * Met `  X
)  /\  y  e.  X )  /\  (
( x  /  2
)  e.  RR*  /\  x  e.  RR*  /\  ( x  /  2 )  < 
x ) )  ->  { z  e.  X  |  ( y D z )  <_  (
x  /  2 ) }  C_  ( y
( ball `  D )
x ) )
194186, 191, 193syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X
)  /\  x  e.  RR+ )  ->  { z  e.  X  |  (
y D z )  <_  ( x  / 
2 ) }  C_  ( y ( ball `  D ) x ) )
195 sstr2 3128 . . . . . . . . . . . 12  |-  ( { z  e.  X  | 
( y D z )  <_  ( x  /  2 ) } 
C_  ( y (
ball `  D )
x )  ->  (
( y ( ball `  D ) x ) 
C_  ( A `  n )  ->  { z  e.  X  |  ( y D z )  <_  ( x  / 
2 ) }  C_  ( A `  n ) ) )
196194, 195syl 17 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X
)  /\  x  e.  RR+ )  ->  ( (
y ( ball `  D
) x )  C_  ( A `  n )  ->  { z  e.  X  |  ( y D z )  <_ 
( x  /  2
) }  C_  ( A `  n )
) )
197187adantl 454 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X
)  /\  x  e.  RR+ )  ->  ( x  /  2 )  e.  RR+ )
198 breq2 3967 . . . . . . . . . . . . . . . 16  |-  ( r  =  ( x  / 
2 )  ->  (
( y D z )  <_  r  <->  ( y D z )  <_ 
( x  /  2
) ) )
199198rabbidv 2732 . . . . . . . . . . . . . . 15  |-  ( r  =  ( x  / 
2 )  ->  { z  e.  X  |  ( y D z )  <_  r }  =  { z  e.  X  |  ( y D z )  <_  (
x  /  2 ) } )
200199sseq1d 3147 . . . . . . . . . . . . . 14  |-  ( r  =  ( x  / 
2 )  ->  ( { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n )  <->  { z  e.  X  |  (
y D z )  <_  ( x  / 
2 ) }  C_  ( A `  n ) ) )
201200rcla4ev 2835 . . . . . . . . . . . . 13  |-  ( ( ( x  /  2
)  e.  RR+  /\  {
z  e.  X  | 
( y D z )  <_  ( x  /  2 ) } 
C_  ( A `  n ) )  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) )
202201ex 425 . . . . . . . . . . . 12  |-  ( ( x  /  2 )  e.  RR+  ->  ( { z  e.  X  | 
( y D z )  <_  ( x  /  2 ) } 
C_  ( A `  n )  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_ 
r }  C_  ( A `  n )
) )
203197, 202syl 17 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X
)  /\  x  e.  RR+ )  ->  ( {
z  e.  X  | 
( y D z )  <_  ( x  /  2 ) } 
C_  ( A `  n )  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_ 
r }  C_  ( A `  n )
) )
204184, 196, 2033syld 53 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X
)  /\  x  e.  RR+ )  ->  ( (
y ( ball `  D
) x )  C_  ( ( int `  J
) `  ( A `  n ) )  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) ) )
205204rexlimdva 2638 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  X )  ->  ( E. x  e.  RR+  (
y ( ball `  D
) x )  C_  ( ( int `  J
) `  ( A `  n ) )  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) ) )
206179, 205syldan 458 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( int `  J
) `  ( A `  n ) ) )  ->  ( E. x  e.  RR+  ( y (
ball `  D )
x )  C_  (
( int `  J
) `  ( A `  n ) )  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) ) )
207175, 206mpd 16 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  ( ( int `  J
) `  ( A `  n ) ) )  ->  E. r  e.  RR+  { z  e.  X  | 
( y D z )  <_  r }  C_  ( A `  n
) )
208207ex 425 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( y  e.  ( ( int `  J ) `  ( A `  n )
)  ->  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_ 
r }  C_  ( A `  n )
) )
209170, 208jcad 521 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( y  e.  ( ( int `  J ) `  ( A `  n )
)  ->  ( y  e.  X  /\  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_ 
r }  C_  ( A `  n )
) ) )
210209eximdv 2019 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ( E. y  y  e.  ( ( int `  J
) `  ( A `  n ) )  ->  E. y ( y  e.  X  /\  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_ 
r }  C_  ( A `  n )
) ) )
211 n0 3406 . . . 4  |-  ( ( ( int `  J
) `  ( A `  n ) )  =/=  (/) 
<->  E. y  y  e.  ( ( int `  J
) `  ( A `  n ) ) )
212 df-rex 2521 . . . 4  |-  ( E. y  e.  X  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n )  <->  E. y ( y  e.  X  /\  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_ 
r }  C_  ( A `  n )
) )
213210, 211, 2123imtr4g 263 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( int `  J
) `  ( A `  n ) )  =/=  (/)  ->  E. y  e.  X  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) ) )
214213reximdva 2626 . 2  |-  ( ph  ->  ( E. n  e.  NN  ( ( int `  J ) `  ( A `  n )
)  =/=  (/)  ->  E. n  e.  NN  E. y  e.  X  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) ) )
215162, 214mpd 16 1  |-  ( ph  ->  E. n  e.  NN  E. y  e.  X  E. r  e.  RR+  { z  e.  X  |  ( y D z )  <_  r }  C_  ( A `  n ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 939   E.wex 1537    = wceq 1619    e. wcel 1621    =/= wne 2419   A.wral 2516   E.wrex 2517   {crab 2519   _Vcvv 2740    C_ wss 3094   (/)c0 3397   ~Pcpw 3566   U.cuni 3768   |^|_ciin 3847   class class class wbr 3963    e. cmpt 4017   `'ccnv 4625   ran crn 4627   "cima 4629    Fn wfn 4633   -->wf 4634   ` cfv 4638  (class class class)co 5757   RRcr 8669   RR*cxr 8799    < clt 8800    <_ cle 8801    / cdiv 9356   NNcn 9679   2c2 9728   RR+crp 10286   * Metcxmt 16296   Metcme 16297   ballcbl 16298   MetOpencmopn 16299   Topctop 16558  TopOnctopon 16559   Clsdccld 16680   intcnt 16681    Cn ccn 16881   CMetcms 18607   NrmCVeccnv 21065   BaseSetcba 21067   0veccn0v 21069   normCVcnmcv 21071   IndMetcims 21072    BLnOp cblo 21245   CBanccbn 21366
This theorem is referenced by:  ubthlem3  21376
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4071  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449  ax-inf2 7275  ax-dc 8005  ax-cnex 8726  ax-resscn 8727  ax-1cn 8728  ax-icn 8729  ax-addcl 8730  ax-addrcl 8731  ax-mulcl 8732  ax-mulrcl 8733  ax-mulcom 8734  ax-addass 8735  ax-mulass 8736  ax-distr 8737  ax-i2m1 8738  ax-1ne0 8739  ax-1rid 8740  ax-rnegex 8741  ax-rrecex 8742  ax-cnre 8743  ax-pre-lttri 8744  ax-pre-lttrn 8745  ax-pre-ltadd 8746  ax-pre-mulgt0 8747  ax-pre-sup 8748  ax-addf 8749  ax-mulf 8750
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2520  df-rex 2521  df-reu 2522  df-rab 2523  df-v 2742  df-sbc 2936  df-csb 3024  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-pss 3110  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-int 3804  df-iun 3848  df-iin 3849  df-br 3964  df-opab 4018  df-mpt 4019  df-tr 4054  df-eprel 4242  df-id 4246  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333  df-lim 4334  df-suc 4335  df-om 4594  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-f1 4651  df-fo 4652  df-f1o 4653  df-fv 4654  df-ov 5760  df-oprab 5761  df-mpt2 5762  df-1st 6021  df-2nd 6022  df-iota 6190  df-riota 6237  df-recs 6321  df-rdg 6356  df-1o 6412  df-er 6593  df-map 6707  df-pm 6708  df-en 6797  df-dom 6798  df-sdom 6799  df-sup 7127  df-pnf 8802  df-mnf 8803  df-xr 8804  df-ltxr 8805  df-le 8806  df-sub 8972  df-neg 8973  df-div 9357  df-n 9680  df-2 9737  df-3 9738  df-n0 9898  df-z 9957  df-uz 10163  df-q 10249  df-rp 10287  df-xneg 10384  df-xadd 10385  df-xmul 10386  df-ico 10593  df-seq 10978  df-exp 11036  df-cj 11514  df-re 11515  df-im 11516  df-sqr 11650  df-abs 11651  df-rest 13254  df-topgen 13271  df-xmet 16300  df-met 16301  df-bl 16302  df-mopn 16303  df-top 16563  df-bases 16565  df-topon 16566  df-cld 16683  df-ntr 16684  df-cls 16685  df-nei 16762  df-cn 16884  df-cnp 16885  df-lm 16886  df-fbas 17447  df-fg 17448  df-fil 17468  df-fm 17560  df-flim 17561  df-flf 17562  df-cfil 18608  df-cau 18609  df-cmet 18610  df-grpo 20783  df-gid 20784  df-ginv 20785  df-gdiv 20786  df-ablo 20874  df-vc 21027  df-nv 21073  df-va 21076  df-ba 21077  df-sm 21078  df-0v 21079  df-vs 21080  df-nmcv 21081  df-ims 21082  df-lno 21247  df-nmoo 21248  df-blo 21249  df-0o 21250  df-cbn 21367
  Copyright terms: Public domain W3C validator