Metamath Proof Explorer

Theorem prdstotbnd

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)

Ref Expression
Hypotheses prdsbnd.y 
|- Y = ( S Xs_ 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 prdstotbnd 
|- ( ph -> D e. ( TotBnd ` B ) )

Proof

Step Hyp Ref Expression
1 prdsbnd.y 
 |-  Y = ( S Xs_ R )
2 prdsbnd.b 
 |-  B = ( Base ` Y )
3 prdsbnd.v 
 |-  V = ( Base ` ( R ` x ) )
4 prdsbnd.e 
 |-  E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )
5 prdsbnd.d 
 |-  D = ( dist ` Y )
6 prdsbnd.s 
 |-  ( ph -> S e. W )
7 prdsbnd.i 
 |-  ( ph -> I e. Fin )
8 prdsbnd.r 
 |-  ( ph -> R Fn I )
9 prdstotbnd.m 
 |-  ( ( ph /\ x e. I ) -> E e. ( TotBnd ` V ) )
10 eqid 
 |-  ( S Xs_ ( x e. I |-> ( R ` x ) ) ) = ( S Xs_ ( x e. I |-> ( R ` x ) ) )
11 eqid 
 |-  ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
12 eqid 
 |-  ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) = ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
13 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. _V )
14 totbndmet 
 |-  ( E e. ( TotBnd ` V ) -> E e. ( Met ` V ) )
15 9 14 syl 
 |-  ( ( ph /\ x e. I ) -> E e. ( Met ` V ) )
16 10 11 3 4 12 6 7 13 15 prdsmet 
 |-  ( ph -> ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) e. ( Met ` ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) ) )
17 dffn5 
 |-  ( R Fn I <-> R = ( x e. I |-> ( R ` x ) ) )
18 8 17 sylib 
 |-  ( ph -> R = ( x e. I |-> ( R ` x ) ) )
19 18 oveq2d 
 |-  ( ph -> ( S Xs_ R ) = ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
20 1 19 eqtrid 
 |-  ( ph -> Y = ( S Xs_ ( x e. I |-> ( R ` x ) ) ) )
21 20 fveq2d 
 |-  ( ph -> ( dist ` Y ) = ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
22 5 21 eqtrid 
 |-  ( ph -> D = ( dist ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
23 20 fveq2d 
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
24 2 23 eqtrid 
 |-  ( ph -> B = ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) )
25 24 fveq2d 
 |-  ( ph -> ( Met ` B ) = ( Met ` ( Base ` ( S Xs_ ( x e. I |-> ( R ` x ) ) ) ) ) )
26 16 22 25 3eltr4d 
 |-  ( ph -> D e. ( Met ` B ) )
27 7 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> I e. Fin )
28 istotbnd3 
 |-  ( 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 ) )
29 28 simprbi 
 |-  ( 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 )
30 9 29 syl 
 |-  ( ( 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 )
31 30 r19.21bi 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( 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 ) )
34 32 33 bitr4i 
 |-  ( 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 ) )
35 31 34 sylib 
 |-  ( ( ( 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 ) )
36 35 an32s 
 |-  ( ( ( 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 ) )
37 36 ralrimiva 
 |-  ( ( 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 
 |-  ( w = ( f ` x ) -> ( w e. ( ~P V i^i Fin ) <-> ( f ` x ) e. ( ~P V i^i Fin ) ) )
39 iuneq1 
 |-  ( w = ( f ` x ) -> U_ z e. w ( z ( ball ` E ) r ) = U_ z e. ( f ` x ) ( z ( ball ` E ) r ) )
40 39 eqeq1d 
 |-  ( w = ( f ` x ) -> ( U_ z e. w ( z ( ball ` E ) r ) = V <-> U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) )
41 38 40 anbi12d 
 |-  ( 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 ) ) )
42 41 ac6sfi 
 |-  ( ( 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 ) ) )
43 27 37 42 syl2anc 
 |-  ( ( 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 
 |-  ( ( f ` x ) e. ( ~P V i^i Fin ) <-> ( ( f ` x ) C_ V /\ ( f ` x ) e. Fin ) )
45 44 simplbi 
 |-  ( ( f ` x ) e. ( ~P V i^i Fin ) -> ( f ` x ) C_ V )
46 45 adantr 
 |-  ( ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> ( f ` x ) C_ V )
47 46 ralimi 
 |-  ( 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 )
48 47 ad2antll 
 |-  ( ( ( 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 
 |-  ( A. x e. I ( f ` x ) C_ V -> X_ x e. I ( f ` x ) C_ X_ x e. I V )
50 48 49 syl 
 |-  ( ( ( 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 
 |-  ( ( R Fn I /\ I e. Fin ) -> R e. Fin )
52 8 7 51 syl2anc 
 |-  ( ph -> R e. Fin )
53 8 fndmd 
 |-  ( ph -> dom R = I )
54 1 6 52 2 53 prdsbas 
 |-  ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
55 3 rgenw 
 |-  A. x e. I V = ( Base ` ( R ` x ) )
56 ixpeq2 
 |-  ( A. x e. I V = ( Base ` ( R ` x ) ) -> X_ x e. I V = X_ x e. I ( Base ` ( R ` x ) ) )
57 55 56 ax-mp 
 |-  X_ x e. I V = X_ x e. I ( Base ` ( R ` x ) )
58 54 57 eqtr4di 
 |-  ( ph -> B = X_ x e. I V )
59 58 ad2antrr 
 |-  ( ( ( 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 )
60 50 59 sseqtrrd 
 |-  ( ( ( 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 )
61 27 adantr 
 |-  ( ( ( 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 )
62 44 simprbi 
 |-  ( ( f ` x ) e. ( ~P V i^i Fin ) -> ( f ` x ) e. Fin )
63 62 adantr 
 |-  ( ( ( f ` x ) e. ( ~P V i^i Fin ) /\ U_ z e. ( f ` x ) ( z ( ball ` E ) r ) = V ) -> ( f ` x ) e. Fin )
64 63 ralimi 
 |-  ( 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 )
65 64 ad2antll 
 |-  ( ( ( 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 )
66 ixpfi 
 |-  ( ( I e. Fin /\ A. x e. I ( f ` x ) e. Fin ) -> X_ x e. I ( f ` x ) e. Fin )
67 61 65 66 syl2anc 
 |-  ( ( ( 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 )
68 elfpw 
 |-  ( 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 ) )
69 60 67 68 sylanbrc 
 |-  ( ( ( 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 ) )
70 metxmet 
 |-  ( D e. ( Met ` B ) -> D e. ( *Met ` B ) )
71 26 70 syl 
 |-  ( ph -> D e. ( *Met ` B ) )
72 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
73 blssm 
 |-  ( ( D e. ( *Met ` B ) /\ y e. B /\ r e. RR* ) -> ( y ( ball ` D ) r ) C_ B )
74 73 3expa 
 |-  ( ( ( D e. ( *Met ` B ) /\ y e. B ) /\ r e. RR* ) -> ( y ( ball ` D ) r ) C_ B )
75 74 an32s 
 |-  ( ( ( D e. ( *Met ` B ) /\ r e. RR* ) /\ y e. B ) -> ( y ( ball ` D ) r ) C_ B )
76 75 ralrimiva 
 |-  ( ( D e. ( *Met ` B ) /\ r e. RR* ) -> A. y e. B ( y ( ball ` D ) r ) C_ B )
77 71 72 76 syl2an 
 |-  ( ( ph /\ r e. RR+ ) -> A. y e. B ( y ( ball ` D ) r ) C_ B )
78 77 adantr 
 |-  ( ( ( 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 )
79 ssralv 
 |-  ( 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 ) )
80 60 78 79 sylc 
 |-  ( ( ( 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 )
81 iunss 
 |-  ( 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 )
82 80 81 sylibr 
 |-  ( ( ( 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 )
83 61 adantr 
 |-  ( ( ( ( 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 )
84 59 eleq2d 
 |-  ( ( ( 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 ) )
85 vex 
 |-  g e. _V
86 85 elixp 
 |-  ( g e. X_ x e. I V <-> ( g Fn I /\ A. x e. I ( g ` x ) e. V ) )
87 86 simprbi 
 |-  ( g e. X_ x e. I V -> A. x e. I ( g ` x ) e. V )
88 df-rex 
 |-  ( 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 ) ) )
89 eliun 
 |-  ( ( g ` x ) e. U_ z e. ( f ` x ) ( z ( ball ` E ) r ) <-> E. z e. ( f ` x ) ( g ` x ) e. ( z ( ball ` E ) r ) )
90 rexv 
 |-  ( 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 ) ) )
91 88 89 90 3bitr4i 
 |-  ( ( 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 ) ) )
92 eleq2 
 |-  ( 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 ) )
93 91 92 bitr3id 
 |-  ( 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 ) )
94 93 biimprd 
 |-  ( 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 ) ) ) )
95 94 adantl 
 |-  ( ( ( 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 ) ) ) )
96 95 ral2imi 
 |-  ( 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 ) ) ) )
97 96 ad2antll 
 |-  ( ( ( 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 ) ) ) )
98 87 97 syl5 
 |-  ( ( ( 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 ) ) ) )
99 84 98 sylbid 
 |-  ( ( ( 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 ) ) ) )
100 99 imp 
 |-  ( ( ( ( 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 ) ) )
101 eleq1 
 |-  ( z = ( y ` x ) -> ( z e. ( f ` x ) <-> ( y ` x ) e. ( f ` x ) ) )
102 oveq1 
 |-  ( z = ( y ` x ) -> ( z ( ball ` E ) r ) = ( ( y ` x ) ( ball ` E ) r ) )
103 102 eleq2d 
 |-  ( z = ( y ` x ) -> ( ( g ` x ) e. ( z ( ball ` E ) r ) <-> ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) )
104 101 103 anbi12d 
 |-  ( 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 ) ) ) )
105 104 ac6sfi 
 |-  ( ( 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 ) ) ) )
106 83 100 105 syl2anc 
 |-  ( ( ( ( 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 ) ) ) )
107 ffn 
 |-  ( y : I --> _V -> y Fn I )
108 simpl 
 |-  ( ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) -> ( y ` x ) e. ( f ` x ) )
109 108 ralimi 
 |-  ( 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 ) )
110 107 109 anim12i 
 |-  ( ( 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 ) ) )
111 vex 
 |-  y e. _V
112 111 elixp 
 |-  ( y e. X_ x e. I ( f ` x ) <-> ( y Fn I /\ A. x e. I ( y ` x ) e. ( f ` x ) ) )
113 110 112 sylibr 
 |-  ( ( 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 ) )
114 113 adantl 
 |-  ( ( ( ( ( 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 ) )
115 84 biimpa 
 |-  ( ( ( ( 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 )
116 ixpfn 
 |-  ( g e. X_ x e. I V -> g Fn I )
117 115 116 syl 
 |-  ( ( ( ( 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 )
118 117 adantr 
 |-  ( ( ( ( ( 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 )
119 simpr 
 |-  ( ( ( y ` x ) e. ( f ` x ) /\ ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) ) -> ( g ` x ) e. ( ( y ` x ) ( ball ` E ) r ) )
120 119 ralimi 
 |-  ( 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 ) )
121 120 ad2antll 
 |-  ( ( ( ( ( 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 ) )
122 85 elixp 
 |-  ( 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 ) ) )
123 118 121 122 sylanbrc 
 |-  ( ( ( ( ( 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 ) )
124 simp-4l 
 |-  ( ( ( ( ( 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 )
125 50 ad2antrr 
 |-  ( ( ( ( ( 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 )
126 125 114 sseldd 
 |-  ( ( ( ( ( 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 )
127 124 58 syl 
 |-  ( ( ( ( ( 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 )
128 126 127 eleqtrrd 
 |-  ( ( ( ( ( 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 )
129 simp-4r 
 |-  ( ( ( ( ( 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+ )
130 fveq2 
 |-  ( y = x -> ( R ` y ) = ( R ` x ) )
131 130 cbvmptv 
 |-  ( y e. I |-> ( R ` y ) ) = ( x e. I |-> ( R ` x ) )
132 131 oveq2i 
 |-  ( S Xs_ ( y e. I |-> ( R ` y ) ) ) = ( S Xs_ ( x e. I |-> ( R ` x ) ) )
133 20 132 eqtr4di 
 |-  ( ph -> Y = ( S Xs_ ( y e. I |-> ( R ` y ) ) ) )
134 133 fveq2d 
 |-  ( ph -> ( dist ` Y ) = ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
135 5 134 eqtrid 
 |-  ( ph -> D = ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
136 135 fveq2d 
 |-  ( ph -> ( ball ` D ) = ( ball ` ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) ) )
137 136 oveqdr 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> ( y ( ball ` D ) r ) = ( y ( ball ` ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) ) r ) )
138 eqid 
 |-  ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) )
139 eqid 
 |-  ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) = ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) )
140 6 adantr 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> S e. W )
141 7 adantr 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> I e. Fin )
142 fvexd 
 |-  ( ( ( ph /\ ( y e. B /\ r e. RR+ ) ) /\ x e. I ) -> ( R ` x ) e. _V )
143 metxmet 
 |-  ( E e. ( Met ` V ) -> E e. ( *Met ` V ) )
144 15 143 syl 
 |-  ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
145 144 adantlr 
 |-  ( ( ( ph /\ ( y e. B /\ r e. RR+ ) ) /\ x e. I ) -> E e. ( *Met ` V ) )
146 simprl 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> y e. B )
147 133 fveq2d 
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
148 2 147 eqtrid 
 |-  ( ph -> B = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
149 148 adantr 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> B = ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
150 146 149 eleqtrd 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> y e. ( Base ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) )
151 72 ad2antll 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> r e. RR* )
152 rpgt0 
 |-  ( r e. RR+ -> 0 < r )
153 152 ad2antll 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> 0 < r )
154 132 138 3 4 139 140 141 142 145 150 151 153 prdsbl 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> ( y ( ball ` ( dist ` ( S Xs_ ( y e. I |-> ( R ` y ) ) ) ) ) r ) = X_ x e. I ( ( y ` x ) ( ball ` E ) r ) )
155 137 154 eqtrd 
 |-  ( ( ph /\ ( y e. B /\ r e. RR+ ) ) -> ( y ( ball ` D ) r ) = X_ x e. I ( ( y ` x ) ( ball ` E ) r ) )
156 124 128 129 155 syl12anc 
 |-  ( ( ( ( ( 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 ) )
157 123 156 eleqtrrd 
 |-  ( ( ( ( ( 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 ) )
158 114 157 jca 
 |-  ( ( ( ( ( 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 ) ) )
159 158 ex 
 |-  ( ( ( ( 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 ) ) ) )
160 159 eximdv 
 |-  ( ( ( ( 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 ) ) ) )
161 df-rex 
 |-  ( 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 ) ) )
162 160 161 imbitrrdi 
 |-  ( ( ( ( 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 ) ) )
163 106 162 mpd 
 |-  ( ( ( ( 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 ) )
164 163 ex 
 |-  ( ( ( 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 ) ) )
165 eliun 
 |-  ( 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 ) )
166 164 165 imbitrrdi 
 |-  ( ( ( 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 ) ) )
167 166 ssrdv 
 |-  ( ( ( 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 ) )
168 82 167 eqssd 
 |-  ( ( ( 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 )
169 iuneq1 
 |-  ( 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 ) )
170 169 eqeq1d 
 |-  ( 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 ) )
171 170 rspcev 
 |-  ( ( 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 )
172 69 168 171 syl2anc 
 |-  ( ( ( 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 )
173 43 172 exlimddv 
 |-  ( ( ph /\ r e. RR+ ) -> E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B )
174 173 ralrimiva 
 |-  ( ph -> A. r e. RR+ E. v e. ( ~P B i^i Fin ) U_ y e. v ( y ( ball ` D ) r ) = B )
175 istotbnd3 
 |-  ( 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 ) )
176 26 174 175 sylanbrc 
 |-  ( ph -> D e. ( TotBnd ` B ) )