Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prdstotbnd Structured version   Visualization version   Unicode version
Theorem prdstotbnd 33593
Description: The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.)
Hypotheses
Ref Expression
prdsbnd.y |- Y = ( S X_s R )
prdsbnd.b |- B = ( Base ` Y )
prdsbnd.v |- V = ( Base ` ( R ` x ) )
prdsbnd.e |- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )
prdsbnd.d |- D = ( dist ` Y )
prdsbnd.s |- ( ph -> S e. W )
prdsbnd.i |- ( ph -> I e. Fin )
prdsbnd.r |- ( ph -> R Fn I )
prdstotbnd.m |- ( ( ph /\ x e. I ) -> E e. ( TotBnd ` V ) )
Assertion
Ref Expression
prdstotbnd |- ( ph -> D e. ( TotBnd ` B ) )
Distinct variable groups:   x, R   x, B   ph, x   x, I   x, S   x, Y
Allowed substitution hints:   D( x)   E( x)   V( x)   W( x)
Proof of Theorem prdstotbnd
Dummy variables z r f g v y w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2622 . . . 4 |- ( S X_s ( x e. I |-> ( R ` x ) ) ) = ( S X_s ( x e. I |-> ( R ` x ) ) )
2 eqid 2622 . . . 4 |- ( Base ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) = ( Base ` ( S X_s ( x e. I |-> ( R ` x ) ) ) )
3 prdsbnd.v . . . 4 |- V = ( Base ` ( R ` x ) )
4 prdsbnd.e . . . 4 |- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )
5 eqid 2622 . . . 4 |- ( dist ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) = ( dist ` ( S X_s ( x e. I |-> ( R ` x ) ) ) )
6 prdsbnd.s . . . 4 |- ( ph -> S e. W )
7 prdsbnd.i . . . 4 |- ( ph -> I e. Fin )
8 fvexd 6203 . . . 4 |- ( ( ph /\ x e. I ) -> ( R ` x ) e. _V )
9 prdstotbnd.m . . . . 5 |- ( ( ph /\ x e. I ) -> E e. ( TotBnd ` V ) )
10 totbndmet 33571 . . . . 5 |- ( E e. ( TotBnd ` V ) -> E e. ( Met ` V ) )
119, 10syl 17 . . . 4 |- ( ( ph /\ x e. I ) -> E e. ( Met ` V ) )
121, 2, 3, 4, 5, 6, 7, 8, 11prdsmet 22175 . . 3 |- ( ph -> ( dist ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) e. ( Met ` ( Base ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) ) )
13 prdsbnd.d . . . 4 |- D = ( dist ` Y )
14 prdsbnd.y . . . . . 6 |- Y = ( S X_s R )
15 prdsbnd.r . . . . . . . 8 |- ( ph -> R Fn I )
16 dffn5 6241 . . . . . . . 8 |- ( R Fn I <-> R = ( x e. I |-> ( R ` x ) ) )
1715, 16sylib 208 . . . . . . 7 |- ( ph -> R = ( x e. I |-> ( R ` x ) ) )
1817oveq2d 6666 . . . . . 6 |- ( ph -> ( S X_s R ) = ( S X_s ( x e. I |-> ( R ` x ) ) ) )
1914, 18syl5eq 2668 . . . . 5 |- ( ph -> Y = ( S X_s ( x e. I |-> ( R ` x ) ) ) )
2019fveq2d 6195 . . . 4 |- ( ph -> ( dist ` Y ) = ( dist ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) )
2113, 20syl5eq 2668 . . 3 |- ( ph -> D = ( dist ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) )
22 prdsbnd.b . . . . 5 |- B = ( Base ` Y )
2319fveq2d 6195 . . . . 5 |- ( ph -> ( Base ` Y ) = ( Base ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) )
2422, 23syl5eq 2668 . . . 4 |- ( ph -> B = ( Base ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) )
2524fveq2d 6195 . . 3 |- ( ph -> ( Met ` B ) = ( Met ` ( Base ` ( S X_s ( x e. I |-> ( R ` x ) ) ) ) ) )
2612, 21, 253eltr4d 2716 . 2 |- ( ph -> D e. ( Met ` B ) )
277adantr 481 . . . . 5 |- ( ( ph /\ r e. RR+ ) -> I e. Fin )
28 istotbnd3 33570 . . . . . . . . . . 11 |- ( E e. ( TotBnd ` V ) <-> ( E e. ( Met ` V ) /\ A. r e. RR+ E. w e. ( ~P V i^i Fin ) U_ z e. w ( z ( ball ` E ) r ) = V ) )
2928simprbi 480 . . . . . . . . . 10 |- ( E e. ( TotBnd ` V ) -> A. r e. RR+ E. w e. ( ~P V i^i Fin ) U_ z e. w ( z ( ball ` E ) r ) = V )
309, 29syl 17 . . . . . . . . 9 |- ( ( ph /\ x e. I ) -> A. r e. RR+ E. w e. ( ~P V i^i Fin ) U_ z e. w ( z ( ball ` E ) r ) = V )
3130r19.21bi 2932 . . . . . . . 8 |- ( ( ( ph /\ x e. I ) /\ r e. RR+ ) -> E. w e. ( ~P V i^i Fin ) U_ z e. w ( z ( ball ` E ) r ) = V )
32 df-rex 2918 . . . . . . . . 9 |- ( E. w e. ( ~P V i^i Fin ) U_ z e. w ( z ( ball ` E ) r ) = V <-> E. w ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) )
33 rexv 3220 . . . . . . . . 9 |- ( E. w e. _V ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) <-> E. w ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) )
3432, 33bitr4i 267 . . . . . . . 8 |- ( E. w e. ( ~P V i^i Fin ) U_ z e. w ( z ( ball ` E ) r ) = V <-> E. w e. _V ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) )
3531, 34sylib 208 . . . . . . 7 |- ( ( ( ph /\ x e. I ) /\ r e. RR+ ) -> E. w e. _V ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) )
3635an32s 846 . . . . . 6 |- ( ( ( ph /\ r e. RR+ ) /\ x e. I ) -> E. w e. _V ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) )
3736ralrimiva 2966 . . . . 5 |- ( ( ph /\ r e. RR+ ) -> A. x e. I E. w e. _V ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) )
38 eleq1 2689 . . . . . . 7 |- ( w = ( f ` x ) -> ( w e. ( ~P V i^i Fin ) <-> ( f ` x ) e. ( ~P V i^i Fin ) ) )
39 iuneq1 4534 . . . . . . . 8 |- ( w = ( f ` x ) -> U_ z e. w ( z ( ball ` E ) r ) = U_ z e. ( f ` x ) ( z ( ball ` E ) r ) )
4039eqeq1d 2624 . . . . . . 7 |- ( w = ( f ` x ) -> ( U_ z e. w ( z ( ball ` E ) r ) = V <-> U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) )
4138, 40anbi12d 747 . . . . . 6 |- ( w = ( f ` x ) -> ( ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) <-> ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) )
4241ac6sfi 8204 . . . . 5 |- ( ( I e. Fin /\ A. x e. I E. w e. _V ( w e. ( ~P V i^i Fin ) /\ U_ z e. w ( z ( ball ` E ) r ) = V ) ) -> E. f ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) )
4327, 37, 42syl2anc 693 . . . 4 |- ( ( ph /\ r e. RR+ ) -> E. f ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) )
44 elfpw 8268 . . . . . . . . . . . 12 |- ( ( f ` x ) e. ( ~P V i^i Fin ) <-> ( ( f ` x ) C_ V /\ ( f ` x ) e. Fin ) )
4544simplbi 476 . . . . . . . . . . 11 |- ( ( f ` x ) e. ( ~P V i^i Fin ) -> ( f ` x ) C_ V )
4645adantr 481 . . . . . . . . . 10 |- ( ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> ( f ` x ) C_ V )
4746ralimi 2952 . . . . . . . . 9 |- ( A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> A. x e. I ( f ` x ) C_ V )
4847ad2antll 765 . . . . . . . 8 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> A. x e. I ( f ` x ) C_ V )
49 ss2ixp 7921 . . . . . . . 8 |- ( A. x e. I ( f ` x ) C_ V -> X_ x e. I ( f ` x ) C_ X_ x e. I V )
5048, 49syl 17 . . . . . . 7 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> X_ x e. I ( f ` x ) C_ X_ x e. I V )
51 fnfi 8238 . . . . . . . . . . 11 |- ( ( R Fn I /\ I e. Fin ) -> R e. Fin )
5215, 7, 51syl2anc 693 . . . . . . . . . 10 |- ( ph -> R e. Fin )
53 fndm 5990 . . . . . . . . . . 11 |- ( R Fn I -> dom R = I )
5415, 53syl 17 . . . . . . . . . 10 |- ( ph -> dom R = I )
5514, 6, 52, 22, 54prdsbas 16117 . . . . . . . . 9 |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
563rgenw 2924 . . . . . . . . . 10 |- A. x e. I V = ( Base ` ( R ` x ) )
57 ixpeq2 7922 . . . . . . . . . 10 |- ( A. x e. I V = ( Base ` ( R ` x ) ) -> X_ x e. I V = X_ x e. I ( Base ` ( R ` x ) ) )
5856, 57ax-mp 5 . . . . . . . . 9 |- X_ x e. I V = X_ x e. I ( Base ` ( R ` x ) )
5955, 58syl6eqr 2674 . . . . . . . 8 |- ( ph -> B = X_ x e. I V )
6059ad2antrr 762 . . . . . . 7 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> B = X_ x e. I V )
6150, 60sseqtr4d 3642 . . . . . 6 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> X_ x e. I ( f ` x ) C_ B )
6227adantr 481 . . . . . . 7 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> I e. Fin )
6344simprbi 480 . . . . . . . . . 10 |- ( ( f ` x ) e. ( ~P V i^i Fin ) -> ( f ` x ) e. Fin )
6463adantr 481 . . . . . . . . 9 |- ( ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> ( f ` x ) e. Fin )
6564ralimi 2952 . . . . . . . 8 |- ( A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> A. x e. I ( f ` x ) e. Fin )
6665ad2antll 765 . . . . . . 7 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> A. x e. I ( f ` x ) e. Fin )
67 ixpfi 8263 . . . . . . 7 |- ( ( I e. Fin /\ A. x e. I ( f ` x ) e. Fin ) -> X_ x e. I ( f ` x ) e. Fin )
6862, 66, 67syl2anc 693 . . . . . 6 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> X_ x e. I ( f ` x ) e. Fin )
69 elfpw 8268 . . . . . 6 |- ( X_ x e. I ( f ` x ) e. ( ~P B i^i Fin ) <-> ( X_ x e. I ( f ` x ) C_ B /\ X_ x e. I ( f ` x ) e. Fin ) )
7061, 68, 69sylanbrc 698 . . . . 5 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> X_ x e. I ( f ` x ) e. ( ~P B i^i Fin ) )
71 metxmet 22139 . . . . . . . . . . 11 |- ( D e. ( Met ` B ) -> D e. ( *Met ` B ) )
7226, 71syl 17 . . . . . . . . . 10 |- ( ph -> D e. ( *Met ` B ) )
73 rpxr 11840 . . . . . . . . . 10 |- ( r e. RR+ -> r e. RR* )
74 blssm 22223 . . . . . . . . . . . . 13 |- ( ( D e. ( *Met ` B ) /\ y e. B /\ r e. RR* ) -> ( y ( ball ` D ) r ) C_ B )
75743expa 1265 . . . . . . . . . . . 12 |- ( ( ( D e. ( *Met ` B ) /\ y e. B ) /\ r e. RR* ) -> ( y ( ball ` D ) r ) C_ B )
7675an32s 846 . . . . . . . . . . 11 |- ( ( ( D e. ( *Met ` B ) /\ r e. RR* ) /\ y e. B ) -> ( y ( ball ` D ) r ) C_ B )
7776ralrimiva 2966 . . . . . . . . . 10 |- ( ( D e. ( *Met ` B ) /\ r e. RR* ) -> A. y e. B ( y ( ball ` D ) r ) C_ B )
7872, 73, 77syl2an 494 . . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> A. y e. B ( y ( ball ` D ) r ) C_ B )
7978adantr 481 . . . . . . . 8 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> A. y e. B ( y ( ball ` D ) r ) C_ B )
80 ssralv 3666 . . . . . . . 8 |- ( X_ x e. I ( f ` x ) C_ B -> ( A. y e. B ( y ( ball ` D ) r ) C_ B -> A. y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) C_ B ) )
8161, 79, 80sylc 65 . . . . . . 7 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> A. y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) C_ B )
82 iunss 4561 . . . . . . 7 |- ( U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) C_ B <-> A. y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) C_ B )
8381, 82sylibr 224 . . . . . 6 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) C_ B )
8462adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> I e. Fin )
8560eleq2d 2687 . . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> ( g e. B <-> g e. X_ x e. I V ) )
86 vex 3203 . . . . . . . . . . . . . . . 16 |- g e. _V
8786elixp 7915 . . . . . . . . . . . . . . 15 |- ( g e. X_ x e. I V <-> ( g Fn I /\ A. x e. I ( g ` x ) e. V ) )
8887simprbi 480 . . . . . . . . . . . . . 14 |- ( g e. X_ x e. I V -> A. x e. I ( g ` x ) e. V )
89 df-rex 2918 . . . . . . . . . . . . . . . . . . . 20 |- ( E. z e. ( f ` x ) ( g ` x ) e. ( z ( ball ` E ) r ) <-> E. z ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) )
90 eliun 4524 . . . . . . . . . . . . . . . . . . . 20 |- ( ( g ` x ) e. U_ z e. ( f ` x ) ( z ( ball ` E ) r ) <-> E. z e. ( f ` x ) ( g ` x ) e. ( z ( ball ` E ) r ) )
91 rexv 3220 . . . . . . . . . . . . . . . . . . . 20 |- ( E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) <-> E. z ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) )
9289, 90, 913bitr4i 292 . . . . . . . . . . . . . . . . . . 19 |- ( ( g ` x ) e. U_ z e. ( f ` x ) ( z ( ball ` E ) r ) <-> E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) )
93 eleq2 2690 . . . . . . . . . . . . . . . . . . 19 |- ( U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V -> ( ( g ` x ) e. U_ z e. ( f ` x ) ( z ( ball ` E ) r ) <-> ( g ` x ) e. V ) )
9492, 93syl5bbr 274 . . . . . . . . . . . . . . . . . 18 |- ( U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V -> ( E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) <-> ( g ` x ) e. V ) )
9594biimprd 238 . . . . . . . . . . . . . . . . 17 |- ( U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V -> ( ( g ` x ) e. V -> E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) )
9695adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> ( ( g ` x ) e. V -> E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) )
9796ral2imi 2947 . . . . . . . . . . . . . . 15 |- ( A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> ( A. x e. I ( g ` x ) e. V -> A. x e. I E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) )
9897ad2antll 765 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> ( A. x e. I ( g ` x ) e. V -> A. x e. I E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) )
9988, 98syl5 34 . . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> ( g e. X_ x e. I V -> A. x e. I E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) )
10085, 99sylbid 230 . . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> ( g e. B -> A. x e. I E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) )
101100imp 445 . . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> A. x e. I E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) )
102 eleq1 2689 . . . . . . . . . . . . 13 |- ( z = ( y ` x ) -> ( z e. ( f ` x ) <-> ( y ` x ) e. ( f ` x ) ) )
103 oveq1 6657 . . . . . . . . . . . . . 14 |- ( z = ( y ` x ) -> ( z ( ball ` E ) r ) = ( ( y ` x ) ( ball ` E ) r ) )
104103eleq2d 2687 . . . . . . . . . . . . 13 |- ( z = ( y ` x ) -> ( ( g ` x ) e. ( z ( ball ` E ) r ) <-> ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) )
105102, 104anbi12d 747 . . . . . . . . . . . 12 |- ( z = ( y ` x ) -> ( ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) <-> ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) )
106105ac6sfi 8204 . . . . . . . . . . 11 |- ( ( I e. Fin /\ A. x e. I E. z e. _V ( z e. ( f ` x ) /\ ( g ` x ) e. ( z ( ball ` E ) r ) ) ) -> E. y ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) )
10784, 101, 106syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> E. y ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) )
108 ffn 6045 . . . . . . . . . . . . . . . . 17 |- ( y : I --> _V -> y Fn I )
109 simpl 473 . . . . . . . . . . . . . . . . . 18 |- ( ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) -> ( y ` x ) e. ( f ` x ) )
110109ralimi 2952 . . . . . . . . . . . . . . . . 17 |- ( A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) -> A. x e. I ( y ` x ) e. ( f ` x ) )
111108, 110anim12i 590 . . . . . . . . . . . . . . . 16 |- ( ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) -> ( y Fn I /\ A. x e. I ( y ` x ) e. ( f ` x ) ) )
112 vex 3203 . . . . . . . . . . . . . . . . 17 |- y e. _V
113112elixp 7915 . . . . . . . . . . . . . . . 16 |- ( y e. X_ x e. I ( f ` x ) <-> ( y Fn I /\ A. x e. I ( y ` x ) e. ( f ` x ) ) )
114111, 113sylibr 224 . . . . . . . . . . . . . . 15 |- ( ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) -> y e. X_ x e. I ( f ` x ) )
115114adantl 482 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> y e. X_ x e. I ( f ` x ) )
11685biimpa 501 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> g e. X_ x e. I V )
117 ixpfn 7914 . . . . . . . . . . . . . . . . . 18 |- ( g e. X_ x e. I V -> g Fn I )
118116, 117syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> g Fn I )
119118adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> g Fn I )
120 simpr 477 . . . . . . . . . . . . . . . . . 18 |- ( ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) -> ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) )
121120ralimi 2952 . . . . . . . . . . . . . . . . 17 |- ( A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) -> A. x e. I ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) )
122121ad2antll 765 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> A. x e. I ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) )
12386elixp 7915 . . . . . . . . . . . . . . . 16 |- ( g e. X_ x e. I ( ( y ` x ) ( ball ` E ) r ) <-> ( g Fn I /\ A. x e. I ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) )
124119, 122, 123sylanbrc 698 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> g e. X_ x e. I ( ( y ` x ) ( ball ` E ) r ) )
125 simp-4l 806 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> ph )
12650ad2antrr 762 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> X_ x e. I ( f ` x ) C_ X_ x e. I V )
127126, 115sseldd 3604 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> y e. X_ x e. I V )
128125, 59syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> B = X_ x e. I V )
129127, 128eleqtrrd 2704 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> y e. B )
130 simp-4r 807 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> r e. RR+ )
131 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = x -> ( R ` y ) = ( R ` x ) )
132131cbvmptv 4750 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. I |-> ( R ` y ) ) = ( x e. I |-> ( R ` x ) )
133132oveq2i 6661 . . . . . . . . . . . . . . . . . . . . . 22 |- ( S X_s ( y e. I |-> ( R ` y ) ) ) = ( S X_s ( x e. I |-> ( R ` x ) ) )
13419, 133syl6eqr 2674 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> Y = ( S X_s ( y e. I |-> ( R ` y ) ) ) )
135134fveq2d 6195 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( dist ` Y ) = ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) )
13613, 135syl5eq 2668 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> D = ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) )
137136fveq2d 6195 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ball ` D ) = ( ball ` ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) ) )
138137oveqdr 6674 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> ( y ( ball ` D ) r ) = ( y ( ball ` ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) ) r ) )
139 eqid 2622 . . . . . . . . . . . . . . . . . 18 |- ( Base ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) = ( Base ` ( S X_s ( y e. I |-> ( R ` y ) ) ) )
140 eqid 2622 . . . . . . . . . . . . . . . . . 18 |- ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) = ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) )
1416adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> S e. W )
1427adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> I e. Fin )
143 fvexd 6203 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( y e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( R ` x ) e. _V )
144 metxmet 22139 . . . . . . . . . . . . . . . . . . . 20 |- ( E e. ( Met ` V ) -> E e. ( *Met ` V ) )
14511, 144syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
146145adantlr 751 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( y e. B /\ r e. RR+ ) ) /\ x e. I ) -> E e. ( *Met ` V ) )
147 simprl 794 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> y e. B )
148134fveq2d 6195 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( Base ` Y ) = ( Base ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) )
14922, 148syl5eq 2668 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> B = ( Base ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) )
150149adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> B = ( Base ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) )
151147, 150eleqtrd 2703 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> y e. ( Base ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) )
15273ad2antll 765 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> r e. RR* )
153 rpgt0 11844 . . . . . . . . . . . . . . . . . . 19 |- ( r e. RR+ -> 0 < r )
154153ad2antll 765 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> 0 < r )
155133, 139, 3, 4, 140, 141, 142, 143, 146, 151, 152, 154prdsbl 22296 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> ( y ( ball ` ( dist ` ( S X_s ( y e. I |-> ( R ` y ) ) ) ) ) r ) = X_ x e. I ( ( y ` x ) ( ball ` E ) r ) )
156138, 155eqtrd 2656 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> ( y ( ball ` D ) r ) = X_ x e. I ( ( y ` x ) ( ball ` E ) r ) )
157125, 129, 130, 156syl12anc 1324 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> ( y ( ball ` D ) r ) = X_ x e. I ( ( y ` x ) ( ball ` E ) r ) )
158124, 157eleqtrrd 2704 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> g e. ( y ( ball ` D ) r ) )
159115, 158jca 554 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) /\ ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) ) -> ( y e. X_ x e. I ( f ` x ) /\ g e. ( y ( ball ` D ) r ) ) )
160159ex 450 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> ( ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) -> ( y e. X_ x e. I ( f ` x ) /\ g e. ( y ( ball ` D ) r ) ) ) )
161160eximdv 1846 . . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> ( E. y ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) -> E. y ( y e. X_ x e. I ( f ` x ) /\ g e. ( y ( ball ` D ) r ) ) ) )
162 df-rex 2918 . . . . . . . . . . 11 |- ( E. y e. X_ x e. I ( f ` x ) g e. ( y ( ball ` D ) r ) <-> E. y ( y e. X_ x e. I ( f ` x ) /\ g e. ( y ( ball ` D ) r ) ) )
163161, 162syl6ibr 242 . . . . . . . . . 10 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> ( E. y ( y : I --> _V /\ A. x e. I ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) ) -> E. y e. X_ x e. I ( f ` x ) g e. ( y ( ball ` D ) r ) ) )
164107, 163mpd 15 . . . . . . . . 9 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) /\ g e. B ) -> E. y e. X_ x e. I ( f ` x ) g e. ( y ( ball ` D ) r ) )
165164ex 450 . . . . . . . 8 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> ( g e. B -> E. y e. X_ x e. I ( f ` x ) g e. ( y ( ball ` D ) r ) ) )
166 eliun 4524 . . . . . . . 8 |- ( g e. U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) <-> E. y e. X_ x e. I ( f ` x ) g e. ( y ( ball ` D ) r ) )
167165, 166syl6ibr 242 . . . . . . 7 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> ( g e. B -> g e. U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) ) )
168167ssrdv 3609 . . . . . 6 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> B C_ U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) )
16983, 168eqssd 3620 . . . . 5 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) = B )
170 iuneq1 4534 . . . . . . 7 |- ( v = X_ x e. I ( f ` x ) -> U_ y e. v ( y ( ball ` D ) r ) = U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) )
171170eqeq1d 2624 . . . . . 6 |- ( v = X_ x e. I ( f ` x ) -> ( U_ y e. v ( y ( ball ` D ) r ) = B <-> U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) = B ) )
172171rspcev 3309 . . . . 5 |- ( ( X_ x e. I ( f ` x ) e. ( ~P B i^i Fin ) /\ U_ y e. X_ x e. I ( f ` x ) ( y ( ball ` D ) r ) = B ) -> E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B )
17370, 169, 172syl2anc 693 . . . 4 |- ( ( ( ph /\ r e. RR+ ) /\ ( f : I --> _V /\ A. x e. I ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) ) ) -> E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B )
17443, 173exlimddv 1863 . . 3 |- ( ( ph /\ r e. RR+ ) -> E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B )
175174ralrimiva 2966 . 2 |- ( ph -> A. r e. RR+ E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B )
176 istotbnd3 33570 . 2 |- ( D e. ( TotBnd ` B ) <-> ( D e. ( Met ` B ) /\ A. r e. RR+ E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B ) )
17726, 175, 176sylanbrc 698 1 |- ( ph -> D e. ( TotBnd ` B ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   |` cres 5116   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   X_cixp 7908   Fincfn 7955   0cc0 9936   RR*cxr 10073   < clt 10074   RR+crp 11832   Basecbs 15857   distcds 15950   X_scprds 16106   *Metcxmt 19731   Metcme 19732   ballcbl 19733   TotBndctotbnd 33565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-icc 12182  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-hom 15966  df-cco 15967  df-prds 16108  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-totbnd 33567
This theorem is referenced by:  prdsbnd2  33594
  Copyright terms: Public domain W3C validator