Metamath Proof Explorer

Theorem ubthlem1

Description: Lemma for ubth . 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 , for some n the set An 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.)

Ref Expression
Hypotheses 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 ubthlem1 
|- ( ph -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )

Proof

Step Hyp Ref Expression
1 ubth.1 
 |-  X = ( BaseSet ` U )
2 ubth.2 
 |-  N = ( normCV ` W )
3 ubthlem.3 
 |-  D = ( IndMet ` U )
4 ubthlem.4 
 |-  J = ( MetOpen ` D )
5 ubthlem.5 
 |-  U e. CBan
6 ubthlem.6 
 |-  W e. NrmCVec
7 ubthlem.7 
 |-  ( ph -> T C_ ( U BLnOp W ) )
8 ubthlem.8 
 |-  ( ph -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
9 ubthlem.9 
 |-  A = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
10 rzal 
 |-  ( T = (/) -> A. t e. T ( N ` ( t ` z ) ) <_ k )
11 10 ralrimivw 
 |-  ( T = (/) -> A. z e. X A. t e. T ( N ` ( t ` z ) ) <_ k )
12 rabid2 
 |-  ( X = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } <-> A. z e. X A. t e. T ( N ` ( t ` z ) ) <_ k )
13 11 12 sylibr 
 |-  ( T = (/) -> X = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
14 13 eqcomd 
 |-  ( T = (/) -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } = X )
15 14 eleq1d 
 |-  ( T = (/) -> ( { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) <-> X e. ( Clsd ` J ) ) )
16 iinrab 
 |-  ( T =/= (/) -> |^|_ t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
17 16 adantl 
 |-  ( ( ( 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 } )
18 id 
 |-  ( T =/= (/) -> T =/= (/) )
19 7 sselda 
 |-  ( ( ph /\ t e. T ) -> t e. ( U BLnOp W ) )
20 eqid 
 |-  ( IndMet ` W ) = ( IndMet ` W )
21 eqid 
 |-  ( MetOpen ` ( IndMet ` W ) ) = ( MetOpen ` ( IndMet ` W ) )
22 eqid 
 |-  ( U BLnOp W ) = ( U BLnOp W )
23 bnnv 
 |-  ( U e. CBan -> U e. NrmCVec )
24 5 23 ax-mp 
 |-  U e. NrmCVec
25 3 20 4 21 22 24 6 blocn2 
 |-  ( t e. ( U BLnOp W ) -> t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) )
26 1 3 cbncms 
 |-  ( U e. CBan -> D e. ( CMet ` X ) )
27 5 26 ax-mp 
 |-  D e. ( CMet ` X )
28 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
29 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
30 27 28 29 mp2b 
 |-  D e. ( *Met ` X )
31 4 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
32 30 31 ax-mp 
 |-  J e. ( TopOn ` X )
33 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
34 33 20 imsxmet 
 |-  ( W e. NrmCVec -> ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) )
35 6 34 ax-mp 
 |-  ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) )
36 21 mopntopon 
 |-  ( ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) -> ( MetOpen ` ( IndMet ` W ) ) e. ( TopOn ` ( BaseSet ` W ) ) )
37 35 36 ax-mp 
 |-  ( MetOpen ` ( IndMet ` W ) ) e. ( TopOn ` ( BaseSet ` W ) )
38 iscncl 
 |-  ( ( 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 ) ) ) )
39 32 37 38 mp2an 
 |-  ( t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) <-> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
40 25 39 sylib 
 |-  ( t e. ( U BLnOp W ) -> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
41 19 40 syl 
 |-  ( ( ph /\ t e. T ) -> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
42 41 simpld 
 |-  ( ( ph /\ t e. T ) -> t : X --> ( BaseSet ` W ) )
43 42 adantlr 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> t : X --> ( BaseSet ` W ) )
44 43 ffvelrnda 
 |-  ( ( ( ( ph /\ k e. NN ) /\ t e. T ) /\ x e. X ) -> ( t ` x ) e. ( BaseSet ` W ) )
45 44 biantrurd 
 |-  ( ( ( ( ph /\ k e. NN ) /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` x ) ) <_ k <-> ( ( t ` x ) e. ( BaseSet ` W ) /\ ( N ` ( t ` x ) ) <_ k ) ) )
46 fveq2 
 |-  ( y = ( t ` x ) -> ( N ` y ) = ( N ` ( t ` x ) ) )
47 46 breq1d 
 |-  ( y = ( t ` x ) -> ( ( N ` y ) <_ k <-> ( N ` ( t ` x ) ) <_ k ) )
48 47 elrab 
 |-  ( ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } <-> ( ( t ` x ) e. ( BaseSet ` W ) /\ ( N ` ( t ` x ) ) <_ k ) )
49 45 48 bitr4di 
 |-  ( ( ( ( ph /\ k e. NN ) /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` x ) ) <_ k <-> ( t ` x ) e. { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) )
50 49 pm5.32da 
 |-  ( ( ( 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 } ) ) )
51 2fveq3 
 |-  ( z = x -> ( N ` ( t ` z ) ) = ( N ` ( t ` x ) ) )
52 51 breq1d 
 |-  ( z = x -> ( ( N ` ( t ` z ) ) <_ k <-> ( N ` ( t ` x ) ) <_ k ) )
53 52 elrab 
 |-  ( x e. { z e. X | ( N ` ( t ` z ) ) <_ k } <-> ( x e. X /\ ( N ` ( t ` x ) ) <_ k ) )
54 53 a1i 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( x e. { z e. X | ( N ` ( t ` z ) ) <_ k } <-> ( x e. X /\ ( N ` ( t ` x ) ) <_ k ) ) )
55 ffn 
 |-  ( t : X --> ( BaseSet ` W ) -> t Fn X )
56 elpreima 
 |-  ( 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 } ) ) )
57 43 55 56 3syl 
 |-  ( ( ( 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 } ) ) )
58 50 54 57 3bitr4d 
 |-  ( ( ( 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 } ) ) )
59 58 eqrdv 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> { z e. X | ( N ` ( t ` z ) ) <_ k } = ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) )
60 imaeq2 
 |-  ( x = { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } -> ( `' t " x ) = ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) )
61 60 eleq1d 
 |-  ( x = { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } -> ( ( `' t " x ) e. ( Clsd ` J ) <-> ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) e. ( Clsd ` J ) ) )
62 41 simprd 
 |-  ( ( ph /\ t e. T ) -> A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) )
63 62 adantlr 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) )
64 nnre 
 |-  ( k e. NN -> k e. RR )
65 64 ad2antlr 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> k e. RR )
66 65 rexrd 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> k e. RR* )
67 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
68 33 67 nvzcl 
 |-  ( W e. NrmCVec -> ( 0vec ` W ) e. ( BaseSet ` W ) )
69 6 68 ax-mp 
 |-  ( 0vec ` W ) e. ( BaseSet ` W )
70 33 67 2 20 nvnd 
 |-  ( ( W e. NrmCVec /\ y e. ( BaseSet ` W ) ) -> ( N ` y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
71 6 70 mpan 
 |-  ( y e. ( BaseSet ` W ) -> ( N ` y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
72 xmetsym 
 |-  ( ( ( 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 ) ) )
73 35 69 72 mp3an12 
 |-  ( y e. ( BaseSet ` W ) -> ( ( 0vec ` W ) ( IndMet ` W ) y ) = ( y ( IndMet ` W ) ( 0vec ` W ) ) )
74 71 73 eqtr4d 
 |-  ( y e. ( BaseSet ` W ) -> ( N ` y ) = ( ( 0vec ` W ) ( IndMet ` W ) y ) )
75 74 breq1d 
 |-  ( y e. ( BaseSet ` W ) -> ( ( N ` y ) <_ k <-> ( ( 0vec ` W ) ( IndMet ` W ) y ) <_ k ) )
76 75 rabbiia 
 |-  { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } = { y e. ( BaseSet ` W ) | ( ( 0vec ` W ) ( IndMet ` W ) y ) <_ k }
77 21 76 blcld 
 |-  ( ( ( 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 ) ) ) )
78 35 69 77 mp3an12 
 |-  ( k e. RR* -> { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) )
79 66 78 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) )
80 61 63 79 rspcdva 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> ( `' t " { y e. ( BaseSet ` W ) | ( N ` y ) <_ k } ) e. ( Clsd ` J ) )
81 59 80 eqeltrd 
 |-  ( ( ( ph /\ k e. NN ) /\ t e. T ) -> { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
82 81 ralrimiva 
 |-  ( ( ph /\ k e. NN ) -> A. t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
83 iincld 
 |-  ( ( 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 ) )
84 18 82 83 syl2anr 
 |-  ( ( ( ph /\ k e. NN ) /\ T =/= (/) ) -> |^|_ t e. T { z e. X | ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
85 17 84 eqeltrrd 
 |-  ( ( ( ph /\ k e. NN ) /\ T =/= (/) ) -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
86 4 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
87 30 86 ax-mp 
 |-  J e. Top
88 32 toponunii 
 |-  X = U. J
89 88 topcld 
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
90 87 89 ax-mp 
 |-  X e. ( Clsd ` J )
91 90 a1i 
 |-  ( ( ph /\ k e. NN ) -> X e. ( Clsd ` J ) )
92 15 85 91 pm2.61ne 
 |-  ( ( ph /\ k e. NN ) -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. ( Clsd ` J ) )
93 92 9 fmptd 
 |-  ( ph -> A : NN --> ( Clsd ` J ) )
94 93 frnd 
 |-  ( ph -> ran A C_ ( Clsd ` J ) )
95 88 cldss2 
 |-  ( Clsd ` J ) C_ ~P X
96 94 95 sstrdi 
 |-  ( ph -> ran A C_ ~P X )
97 sspwuni 
 |-  ( ran A C_ ~P X <-> U. ran A C_ X )
98 96 97 sylib 
 |-  ( ph -> U. ran A C_ X )
99 arch 
 |-  ( c e. RR -> E. k e. NN c < k )
100 99 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ c e. RR ) -> E. k e. NN c < k )
101 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. RR ) -> c e. RR )
102 ltle 
 |-  ( ( c e. RR /\ k e. RR ) -> ( c < k -> c <_ k ) )
103 101 64 102 syl2an 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ k e. NN ) -> ( c < k -> c <_ k ) )
104 103 impr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) -> c <_ k )
105 104 adantr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> c <_ k )
106 42 ffvelrnda 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` x ) e. ( BaseSet ` W ) )
107 106 an32s 
 |-  ( ( ( ph /\ x e. X ) /\ t e. T ) -> ( t ` x ) e. ( BaseSet ` W ) )
108 33 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( t ` x ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` x ) ) e. RR )
109 6 107 108 sylancr 
 |-  ( ( ( ph /\ x e. X ) /\ t e. T ) -> ( N ` ( t ` x ) ) e. RR )
110 109 adantlr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ t e. T ) -> ( N ` ( t ` x ) ) e. RR )
111 110 adantlr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> ( N ` ( t ` x ) ) e. RR )
112 simpllr 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> c e. RR )
113 simplrl 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> k e. NN )
114 113 64 syl 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> k e. RR )
115 letr 
 |-  ( ( ( N ` ( t ` x ) ) e. RR /\ c e. RR /\ k e. RR ) -> ( ( ( N ` ( t ` x ) ) <_ c /\ c <_ k ) -> ( N ` ( t ` x ) ) <_ k ) )
116 111 112 114 115 syl3anc 
 |-  ( ( ( ( ( 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 ) )
117 105 116 mpan2d 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ ( k e. NN /\ c < k ) ) /\ t e. T ) -> ( ( N ` ( t ` x ) ) <_ c -> ( N ` ( t ` x ) ) <_ k ) )
118 117 ralimdva 
 |-  ( ( ( ( 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 ) )
119 118 expr 
 |-  ( ( ( ( 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 ) ) )
120 1 fvexi 
 |-  X e. _V
121 120 rabex 
 |-  { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } e. _V
122 9 fvmpt2 
 |-  ( ( 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 } )
123 121 122 mpan2 
 |-  ( k e. NN -> ( A ` k ) = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
124 123 eleq2d 
 |-  ( k e. NN -> ( x e. ( A ` k ) <-> x e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } ) )
125 52 ralbidv 
 |-  ( z = x -> ( A. t e. T ( N ` ( t ` z ) ) <_ k <-> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
126 125 elrab 
 |-  ( x e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } <-> ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) )
127 124 126 bitrdi 
 |-  ( k e. NN -> ( x e. ( A ` k ) <-> ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) ) )
128 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
129 128 biantrurd 
 |-  ( ( ph /\ x e. X ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ k <-> ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) ) )
130 129 bicomd 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X /\ A. t e. T ( N ` ( t ` x ) ) <_ k ) <-> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
131 127 130 sylan9bbr 
 |-  ( ( ( ph /\ x e. X ) /\ k e. NN ) -> ( x e. ( A ` k ) <-> A. t e. T ( N ` ( t ` x ) ) <_ k ) )
132 93 ffnd 
 |-  ( ph -> A Fn NN )
133 132 adantr 
 |-  ( ( ph /\ x e. X ) -> A Fn NN )
134 fnfvelrn 
 |-  ( ( A Fn NN /\ k e. NN ) -> ( A ` k ) e. ran A )
135 elssuni 
 |-  ( ( A ` k ) e. ran A -> ( A ` k ) C_ U. ran A )
136 134 135 syl 
 |-  ( ( A Fn NN /\ k e. NN ) -> ( A ` k ) C_ U. ran A )
137 136 sseld 
 |-  ( ( A Fn NN /\ k e. NN ) -> ( x e. ( A ` k ) -> x e. U. ran A ) )
138 133 137 sylan 
 |-  ( ( ( ph /\ x e. X ) /\ k e. NN ) -> ( x e. ( A ` k ) -> x e. U. ran A ) )
139 131 138 sylbird 
 |-  ( ( ( ph /\ x e. X ) /\ k e. NN ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ k -> x e. U. ran A ) )
140 139 adantlr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. RR ) /\ k e. NN ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ k -> x e. U. ran A ) )
141 119 140 syl6d 
 |-  ( ( ( ( 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 ) ) )
142 141 rexlimdva 
 |-  ( ( ( 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 ) ) )
143 100 142 mpd 
 |-  ( ( ( ph /\ x e. X ) /\ c e. RR ) -> ( A. t e. T ( N ` ( t ` x ) ) <_ c -> x e. U. ran A ) )
144 143 rexlimdva 
 |-  ( ( ph /\ x e. X ) -> ( E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c -> x e. U. ran A ) )
145 144 ralimdva 
 |-  ( 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 ) )
146 8 145 mpd 
 |-  ( ph -> A. x e. X x e. U. ran A )
147 dfss3 
 |-  ( X C_ U. ran A <-> A. x e. X x e. U. ran A )
148 146 147 sylibr 
 |-  ( ph -> X C_ U. ran A )
149 98 148 eqssd 
 |-  ( ph -> U. ran A = X )
150 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
151 1 150 nvzcl 
 |-  ( U e. NrmCVec -> ( 0vec ` U ) e. X )
152 ne0i 
 |-  ( ( 0vec ` U ) e. X -> X =/= (/) )
153 24 151 152 mp2b 
 |-  X =/= (/)
154 4 bcth2 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( A : NN --> ( Clsd ` J ) /\ U. ran A = X ) ) -> E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) )
155 27 153 154 mpanl12 
 |-  ( ( A : NN --> ( Clsd ` J ) /\ U. ran A = X ) -> E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) )
156 93 149 155 syl2anc 
 |-  ( ph -> E. n e. NN ( ( int ` J ) ` ( A ` n ) ) =/= (/) )
157 ffvelrn 
 |-  ( ( A : NN --> ( Clsd ` J ) /\ n e. NN ) -> ( A ` n ) e. ( Clsd ` J ) )
158 95 157 sselid 
 |-  ( ( A : NN --> ( Clsd ` J ) /\ n e. NN ) -> ( A ` n ) e. ~P X )
159 158 elpwid 
 |-  ( ( A : NN --> ( Clsd ` J ) /\ n e. NN ) -> ( A ` n ) C_ X )
160 93 159 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) C_ X )
161 88 ntrss3 
 |-  ( ( J e. Top /\ ( A ` n ) C_ X ) -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
162 87 160 161 sylancr 
 |-  ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
163 162 sseld 
 |-  ( ( ph /\ n e. NN ) -> ( y e. ( ( int ` J ) ` ( A ` n ) ) -> y e. X ) )
164 88 ntropn 
 |-  ( ( J e. Top /\ ( A ` n ) C_ X ) -> ( ( int ` J ) ` ( A ` n ) ) e. J )
165 87 160 164 sylancr 
 |-  ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) e. J )
166 4 mopni2 
 |-  ( ( 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 ) ) )
167 30 166 mp3an1 
 |-  ( ( ( ( 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 ) ) )
168 165 167 sylan 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> E. x e. RR+ ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) )
169 elssuni 
 |-  ( ( ( int ` J ) ` ( A ` n ) ) e. J -> ( ( int ` J ) ` ( A ` n ) ) C_ U. J )
170 169 88 sseqtrrdi 
 |-  ( ( ( int ` J ) ` ( A ` n ) ) e. J -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
171 165 170 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) C_ X )
172 171 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> y e. X )
173 88 ntrss2 
 |-  ( ( J e. Top /\ ( A ` n ) C_ X ) -> ( ( int ` J ) ` ( A ` n ) ) C_ ( A ` n ) )
174 87 160 173 sylancr 
 |-  ( ( ph /\ n e. NN ) -> ( ( int ` J ) ` ( A ` n ) ) C_ ( A ` n ) )
175 sstr2 
 |-  ( ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> ( ( ( int ` J ) ` ( A ` n ) ) C_ ( A ` n ) -> ( y ( ball ` D ) x ) C_ ( A ` n ) ) )
176 174 175 syl5com 
 |-  ( ( ph /\ n e. NN ) -> ( ( y ( ball ` D ) x ) C_ ( ( int ` J ) ` ( A ` n ) ) -> ( y ( ball ` D ) x ) C_ ( A ` n ) ) )
177 176 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
178 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. X ) -> y e. X )
179 178 30 jctil 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. X ) -> ( D e. ( *Met ` X ) /\ y e. X ) )
180 rphalfcl 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
181 180 rpxrd 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR* )
182 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
183 rphalflt 
 |-  ( x e. RR+ -> ( x / 2 ) < x )
184 181 182 183 3jca 
 |-  ( x e. RR+ -> ( ( x / 2 ) e. RR* /\ x e. RR* /\ ( x / 2 ) < x ) )
185 eqid 
 |-  { z e. X | ( y D z ) <_ ( x / 2 ) } = { z e. X | ( y D z ) <_ ( x / 2 ) }
186 4 185 blsscls2 
 |-  ( ( ( 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 ) )
187 179 184 186 syl2an 
 |-  ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( y ( ball ` D ) x ) )
188 sstr2 
 |-  ( { 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 ) ) )
189 187 188 syl 
 |-  ( ( ( ( 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 ) ) )
190 180 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ y e. X ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
191 breq2 
 |-  ( r = ( x / 2 ) -> ( ( y D z ) <_ r <-> ( y D z ) <_ ( x / 2 ) ) )
192 191 rabbidv 
 |-  ( r = ( x / 2 ) -> { z e. X | ( y D z ) <_ r } = { z e. X | ( y D z ) <_ ( x / 2 ) } )
193 192 sseq1d 
 |-  ( r = ( x / 2 ) -> ( { z e. X | ( y D z ) <_ r } C_ ( A ` n ) <-> { z e. X | ( y D z ) <_ ( x / 2 ) } C_ ( A ` n ) ) )
194 193 rspcev 
 |-  ( ( ( 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 ) )
195 194 ex 
 |-  ( ( 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 ) ) )
196 190 195 syl 
 |-  ( ( ( ( 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 ) ) )
197 177 189 196 3syld 
 |-  ( ( ( ( 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 ) ) )
198 197 rexlimdva 
 |-  ( ( ( 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 ) ) )
199 172 198 syldan 
 |-  ( ( ( 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 ) ) )
200 168 199 mpd 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. ( ( int ` J ) ` ( A ` n ) ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )
201 200 ex 
 |-  ( ( ph /\ n e. NN ) -> ( y e. ( ( int ` J ) ` ( A ` n ) ) -> E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) ) )
202 163 201 jcad 
 |-  ( ( 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 ) ) ) )
203 202 eximdv 
 |-  ( ( 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 ) ) ) )
204 n0 
 |-  ( ( ( int ` J ) ` ( A ` n ) ) =/= (/) <-> E. y y e. ( ( int ` J ) ` ( A ` n ) ) )
205 df-rex 
 |-  ( 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 ) ) )
206 203 204 205 3imtr4g 
 |-  ( ( 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 ) ) )
207 206 reximdva 
 |-  ( 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 ) ) )
208 156 207 mpd 
 |-  ( ph -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( A ` n ) )